On the Expressiveness of Real and Integer Arithmetic Automata

If read digit by digit, a n-dimensional vector of integers
represented in base r can be viewed as a word over the alphabet
r to the n. It has been known for some time that, under this encoding, the
sets of integer vectors recognizable by finite automata are exactly
those definable in Presburger arithmetic if independence with respect
to the base is required, and those definable in a slight extension of
Presburger arithmetic if only a specific base is considered.

Using the same encoding idea, but moving to infinite words, finite
automata on infinite words can recognize sets of real vectors. This
leads to the question of which sets of real vectors are recognizable
by finite automata, which is the topic of this paper. We show that
the recognizable sets of real vectors are those definable in the
theory of reals and integers with addition and order, extended with a
special base-dependent predicate that tests the value of a specified
digit of a number. Furthermore, in the course of proving that sets
of vectors defined in this theory are recognizable by finite
automata, we show that linear equations and inequations have
surprisingly compact representations by automata, which leads us to
believe that automata accepting sets of real vectors can be of more
than theoretical interest.