Deciding reachability in automata on words indexed by the reals and rationals

Automata on linear orderings generalize the notions of finite-word and infinite-word automata. They recognize words indexed by linear orderings, defined as mappings from the elements of such orderings to a finite alphabet. The reachability problem has already been solved for automata on scattered linear orderings, i.e., those that do not involve density, as well as for automata over all linear orderings. The main contribution of this work is to provide a polynomial algorithm that decides reachability over the specific linear orderings R and Q. Given an automaton on linear orderings and a pair (p, q) of its states, this procedure decides in polynomial time whether this automaton admits a path from p to q labeled by a word indexed by R or Q. This also solves the non-emptiness problem for the language accepted by these automata restricted to the orderings of the reals and rationals. This algorithm constitutes an essential step towards designing an automata-based decision procedure for the first-order monadic theory of order interpreted over R or Q.