Bernard Boigelot
email: boigelot@montefiore.ulg.ac.be

Julien Brusten
email: brusten@montefiore.ulg.ac.be

Jérôme Leroux
email: leroux@labri.fr

A Generalization of Semenov's Theorem to Automata over Real Numbers ⋆

This work studies the properties of finite automata recognizing vectors with real components, encoded positionally in a given integer numeration base. Such automata are used, in particular, as symbolic data structures for representing sets definable in the first-order theory R, Z, +, ≤ , i.e., the mixed additive arithmetic of integer and real variables. They also lead to a simple decision procedure for this arithmetic.

In previous work, it has been established that the sets definable in R, Z, +, ≤ can be handled by a restricted form of infinite-word automata, weak deterministic ones, regardless of the chosen numeration base. In this paper, we address the reciprocal property, proving that the sets of vectors that are simultaneously recognizable in all bases, by either weak deterministic or Muller automata, are those definable in R, Z, +, ≤ . This result can be seen as a generalization to the mixed integer and real domain of Semenov's theorem, which characterizes the sets of integer vectors recognizable by finite automata in multiple bases. It also extends to multidimensional vectors a similar property recently established for sets of numbers.

As an additional contribution, the techniques used for obtaining our main result lead to valuable insight into the internal structure of automata recognizing sets of vectors definable in R, Z, +, ≤ . This structure might be exploited in order to improve the efficiency of representation systems and decision procedures for this arithmetic.

Introduction

In the program analysis and verification field, one often faces the problem of finding a suitable formalism for expressing the constraints to be satisfied by the system configurations. Ideally, this formalism has to be decidable, while still remaining expressive enough for handling the class of constraints needed by the application. An example of such formalism is Presburger arithmetic, i.e., the firstorder additive theory of integers Z, +, ≤ , which is widely used for reasoning about programs manipulating integer variables. Presburger arithmetic is indeed decidable [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF][START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF], yet expressive enough for describing arbitrary linear constraints as well as discrete periodicities [START_REF] Bruyère | Logic and p-recognizable sets of integers[END_REF].

A simple approach to deciding Presburger arithmetic consists in using finite automata. It is indeed known that, using the positional notation for encoding numbers and vectors into words, all Presburger-definable sets are mapped onto regular languages and can thus be recognized by automata [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF][START_REF] Bruyère | Logic and p-recognizable sets of integers[END_REF]. A Presburger formula can be decided by recursively constructing an automaton recognizing its solutions, and then checking whether this automaton accepts a nonempty language. In some program verification applications, such automata, called Number Decision Diagrams (NDDs) are actually used as data structures for representing and manipulating symbolically the sets of program configurations that need to be handled [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF].

Although every subset of Z n that is Presburger-definable can be recognized by a finite automaton, the reciprocal property does not hold. For instance, denoting by r ∈ N >1 the base chosen for encoding numbers, the set {r k | k ∈ N}, which is not Presburger-definable, clearly corresponds to a regular language and is thus recognizable. The well-known Cobham's theorem states that, if a set S ⊆ Z is simultaneously recognizable by finite automata in two bases r, s ∈ N >1 that are multiplicatively independent, i.e., such that r p = s q for all p, q ∈ N >0 , then S is Presburger definable [START_REF] Cobham | On the base-dependence of sets of numbers recognizable by finite automata[END_REF]. This result has then been extended to subsets of Z n , with n > 0, i.e., sets of integer vectors, by Semenov [START_REF] Semenov | Presburgerness of predicates regular in two number systems[END_REF]. As a corollary of Semenov's theorem, the subsets of Z n that are recognizable by finite automata in every base r ∈ N >1 are exactly those that are Presburger-definable.

Quite recently, automata recognizing sets of numbers and vectors have been generalized to the mixed integer and real domain [START_REF] Boigelot | An improved reachability analysis method for strongly linear hybrid systems[END_REF]. In this setting, the base-r encoding of numbers and vectors take the form of infinite words over the alphabet {0, 1, . . . , r -1, ⋆}, where "⋆" is a separator symbol used for distinguishing their integer and fractional parts. A Real Vector Automaton (RVA) recognizing a set S ⊆ R n is then an infinite-word automaton that accepts the encodings of the elements of S.

It is worth stressing out that RVA are not only theoretical objects; they are used as actual data structures in verification tools such as LASH for representing symbolically the sets of configurations of programs relying on both integer and real variables during their state-space exploration [START_REF]The Liège Automata-based Symbolic Handler (LASH)[END_REF]. The decision tool LIRA also uses RVA for representing the set of solutions of mixed real and integer arithmetic formulas [START_REF] Becker | LIRA: Handling constraints of linear arithmetics over the integers and the reals[END_REF]. For such applications, it is not sufficient to establish that all sets of interest are representable by RVA and that all the needed operations are computable on them, but also to obtain a symbolic representation system that is concise enough for handling complex sets using a reasonable amount of memory, and for which the manipulation algorithms are efficient. In particular, this precludes the use of unrestricted infinite-word automata for describing RVA, due to the difficulty of carrying out some operations such as set complementation [START_REF] Vardi | The Büchi complementation saga[END_REF]. It is therefore essential to define restricted forms of RVA that can be efficiently handled, and to precisely characterize their expressiveness in order to match the requirements of the intended applications. Another goal is to investigate whether the transition relation of these restricted RVA has structural properties that can be exploited in order to represent them more efficiently.

In previous work, a result analogous to Cobham's theorem has been obtained for RVA: The sets S ⊆ R that are recognizable by RVA in two bases that do not share the same set of prime factors1 are exactly those that are definable in the first-order theory R, Z, +, ≤ , i.e., the extension of Presburger arithmetic to mixed integer and real variables [START_REF] Boigelot | On the sets of real numbers recognized by finite automata in multiple bases[END_REF]. This has an important consequence. One indeed knows that the full expressive power of ω-regular languages is not needed for representing the sets definable in R, Z, +, ≤ , since those sets can be recognized by weak deterministic automata [START_REF] Boigelot | An effective decision procedure for linear arithmetic over the integers and reals[END_REF], a restricted class of infinite-word automata that are much more easily manipulated algorithmically, and admit a canonical form. It follows that the sets of reals that are recognizable by RVA in every base r ∈ N >1 are exactly those that can be recognized by weak deterministic RVA. This paper is aimed at extending this result to sets of vectors with a fixed dimension, i.e., to subsets of R n with n > 0. This can be seen as a generalization of Semenov's theorem to real vectors. Precisely, we prove that the sets S ⊆ R n that are simultaneously recognizable by RVA in two bases that do not share the same set of prime factors are those that are definable in R, Z, +, ≤ . From this result, it follows that the sets of vectors that are recognizable by RVA in every base r ∈ N >1 are exactly those that can be recognized by weak deterministic RVA. The same proof also establishes that the sets that are recognizable by weak deterministic RVA in two multiplicatively independent bases are definable in R, Z, +, ≤ as well. Those results are significant for practical applications, since they imply that weak deterministic automata can be used for implementing RVA in all cases where the sets of vectors that are symbolically represented are expressed as combinations of linear constraints and discrete periodicities.

As an additional contribution, the techniques used for obtaining this result give out valuable insight into the internal structure of RVA recognizing sets of vectors definable in R, Z, +, ≤ . It might be possible to exploit this structure in order to improve the efficiency of symbolic representation systems and decision procedures for that arithmetic.

Preliminaries

Positional Encoding of Vectors

Let r ∈ N >1 be a base. The positional notation in base r encodes numbers x ∈ R as infinite words of the form w I ⋆ w F over the finite alphabet Σ r ∪ {⋆}, where Σ r = {0, 1, . . . , r -1}, and "⋆" is a separator symbol. The finite prefix w I ∈ Σ + r and the infinite suffix w F ∈ Σ ω r respectively encode an integer and a fractional part of x. In other words, w I encodes a number x I ∈ Z, and w F a number x F ∈ [0, 1], such that x I + x F = x. Note that integer numbers admit two decompositions into integer and fractional parts, e.g., x = 2 leads to both x I = 2 and x F = 0, and x I = 1 and x F = 1.

An encoding w I of an integer part x I ∈ N is a word a p-1 a p-2 . . . a 0 ∈ Σ + r , with p > 0, such that x I = p-1 i=0 a i r i . For signed numbers x I ∈ Z, the r'scomplement representation is used, implying that the sign digit a p-1 is then equal to 0 for positive (or zero) numbers, and to r -1 for negative ones. For a negative number, the value of x I becomes equal to -r p + p-1 i=0 a i r i . The length p of encodings is not fixed, but chosen large enough for satisfying the constraint -r p-1 ≤ x I < r p-1 . Finally, an encoding w F of a fractional part

x F ∈ [0, 1] is a word b 0 b 1 . . . ∈ Σ ω r such that x F = i≥0 b i r -i
. This encoding scheme can be extended to vectors x = (x 1 , x 2 , . . . , x n ) ∈ R n , with n > 0. The idea is to encode each component x i separately into a word w i , but in such a way that these words share the same integer-part length. This can always be achieved, for the sign digit of an encoding can be repeated at will without altering the encoded value. One thus obtains a vector (w 1 , w 2 , . . . , w n ) of encodings in which the separator symbol "⋆" occurs at the same position in each component. By reading those components synchronously one symbol at a time, one eventually obtains an encoding of x as a single word w I ⋆ w F over the n-dimensional alphabet Σ n r , augmented with a unique separator symbol "⋆". For each word w ∈ {0, r -1} n (Σ n r ) * ⋆ (Σ n r ) ω , the vector x ∈ R n encoded by w in base r is denoted by [w] r .

Real Vector Automata

Consider a base r ∈ N >1 and a set S ⊆ R n , with n > 0. Let L(S) ⊆ (Σ n r ) + ⋆(Σ n r ) ω denote the language formed by the encodings of the elements of S. If L(S) is ω-regular, then any infinite-word automaton that accepts L(S) is a Real Vector Automaton (RVA) recognizing S [START_REF] Boigelot | An improved reachability analysis method for strongly linear hybrid systems[END_REF]. In this paper, in order to simplify some developments thanks to their deterministic transition relation, we assume w.l.o.g. that RVA take the form of Muller automata [START_REF]Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics[END_REF]. A set S ⊆ R n that can be recognized by a RVA in base r is said to be r-recognizable.

For practical applications as symbolic representations of sets, infinite-word automata are somehow problematic, since some of their manipulation algorithms are known to be significantly costlier than their finite-word counterparts [START_REF] Vardi | The Büchi complementation saga[END_REF]. In the case of RVA, its has been shown that the full expressive power of infinite-word automata is not needed for recognizing the sets definable in the first-order theory R, Z, +, ≤ . Indeed, for any base r ∈ N >1 , such sets can be recognized by weak deterministic RVA [START_REF] Boigelot | An effective decision procedure for linear arithmetic over the integers and reals[END_REF]. A weak RVA representing a set S is a Büchi automaton accepting L(S), such that each of its strongly connected components is either globally accepting or globally non-accepting. Compared to general infinite-word automata, weak deterministic ones are much more easily manipulated algorithmically. In addition, they admit a canonical form that simplifies comparison operations between symbolically represented sets [START_REF] Löding | Efficient minimization of deterministic weak ω-automata[END_REF]. We will say that a set S ⊆ R n that can be recognized by a weak deterministic RVA in base r is weakly r-recognizable.

Properties of Recognizable Sets

In the next sections, we study the properties of sets that are recognizable, or weakly recognizable, in one or several bases. Such sets are characterized by the following results.

Theorem 1 ([15]

). Let n ∈ N >0 and r ∈ N >1 . A set S ⊆ R n is r-recognizable iff it is definable in the first-order theory R, Z, +, ≤, X r , where X r ⊂ R 3 is a base-dependent predicate such that X r (x, u, k) holds whenever u is an integer power of r, and there exists an encoding of x in which the digit at the position specified by u is equal to k.

Theorem 2 ([11]

). Let n ∈ N >0 and r ∈ N >1 . A set S ⊆ R n is weakly rrecognizable iff it is r-recognizable, and it belongs to the topological class F σ ∩ G δ of the metric topology over R n induced by the Euclidean distance. This means that the set has to be decomposable both into a countable union of closed sets, and into a countable intersection of open sets.

In particular, it is known that every subset of R n that is definable in the first-order theory R, Z, +, ≤ , i.e., the extension of Presburger arithmetic to mixed integer and real variables, satisfies the hypotheses of Theorem 2, and it is therefore weakly recognizable in every base r ∈ N >1 [START_REF] Boigelot | An effective decision procedure for linear arithmetic over the integers and reals[END_REF].

The following theorems and lemmas introduce some operations and transformations that preserve the recognizable nature of sets. Theorem 3. Let n ∈ N >0 be a dimension, and r, s ∈ N >1 be multiplicatively dependent bases, i.e., such that r k = s l for some k, l ∈ N >0 . A set S ⊆ R n is (resp. weakly) r-recognizable iff it is (resp. weakly) s-recognizable.

Proof sketch. From Theorems 1 and 2, it suffices to show that definability in R, Z, +, ≤, X r is equivalent to definability in R, Z, +, ≤, X s . Furthermore, since r k = s l , it actually suffices to establish that definability in R, Z, +, ≤, X t is equivalent to definability in R, Z, +, ≤, X t i for all t ∈ N >1 and i ∈ N >0 . An encoding of a number x ∈ R in base t i can directly be turned into one of the same number in base t by replacing each digit (belonging to the alphabet Σ t i ) into a sequence of i digits from Σ t . The reciprocal operation is similar. It follows that the predicate X t can be defined in terms of X t i , and reciprocally.

⊓ ⊔ Theorem 3 states that (resp. weak) recognizability in bases that are multiplicatively dependent is equivalent to (resp. weak) recognizability in one of them. In the sequel, we will thus only consider bases r and s that are multiplicatively independent.

Lemma 1. Let n ∈ N >0 , S 1 , S 2 ⊆ R n , and r ∈ N >1 . If S 1 and S 2 are both (resp. weakly) r-recognizable, then the sets S 1 ∪ S 2 , S 1 ∩ S 2 , S 1 \ S 2 and S 1 × S 2 are (resp. weakly) r-recognizable as well.

Proof sketch. The class of sets definable in R, Z, +, ≤, X r is closed under Boolean and Cartesian operators. The same property holds for the topological class F σ ∩ G δ . The result then follows from Theorems 1 and 2.

⊓ ⊔

Lemma 2. Let n ∈ N >0 , r ∈ N >1 , C ∈ Q n×n such that det(C) = 0, and a ∈ Q n . If a set S ⊆ R n is (resp.
weakly) r-recognizable, then the set CS + a is (resp. weakly) r-recognizable as well.

Proof sketch. The proof is by similar arguments as in that of Lemma 1. Indeed, the transformation x → Cx + a is definable in R, Z, +, ≤, X r , and preserves the topological class F σ ∩ G δ . ⊓ ⊔ It is worth mentioning that, in the statement of Lemma 2, it is essential to require det(C) = 0 as far as weak recognizability is concerned. Indeed, a transformation x → Cx + a with a singular matrix C amounts to a projection, which generally alters topological properties of sets. As an example, the set S = {(zr k , r k ) | k, z ∈ Z} belongs to F σ ∩ G δ , and it is actually weakly rrecognizable, whereas the set CS, with C = diag(1, 0), does not.

Although projection does not preserve weak recognizability, one can however sometimes extract from a set a weak recognizable set of smaller dimension. This operation is described by the following lemma.

Lemma 3. Let n, m ∈ N >0 , r ∈ N >1 . If two sets S 1 ⊆ R n and S 2 ⊆ R m are such that S 1 × S 2
is weakly r-recognizable, then S 1 and S 2 are weakly r-recognizable as well.

Proof sketch. The proof is by similar arguments as in that of Lemma 1.

⊓ ⊔ Finally, the following result addresses the comparison of two recognizable sets.

Theorem 4. Let n ∈ N >0 and r ∈ N >1 . Two r-recognizable sets S 1 , S 2 ⊆ R n are equal iff they coincide over the rational vectors, i.e., iff

S 1 ∩ Q n = S 2 ∩ Q n .
Proof sketch. The vectors in Q n are exactly those that are encoded by ultimately periodic words, i.e., words of the form uv ω with |v| ≥ 1. Two ω-regular languages are equal iff they coincide over the ultimately periodic words [START_REF] Perrin | Infinite words[END_REF].

⊓ ⊔ As a corollary, one can always extract a rational vector from a non-empty r-recognizable set.

Problem Reductions

Our main goal will be to prove that a set S ⊆ R n that is recognizable or weakly recognizable in two bases r and s that are multiplicatively independent, with some possible additional restrictions on r and s, is necessarily definable in R, Z, +, ≤ . In this section, we reduce this general problem to simpler ones.

Reduction to [0, 1] n

It is known that a set S ⊆ R n that is r-recognizable can be decomposed into a finite union S = i (S I i + S F i ), where the sets S I i ⊆ Z n are non-empty and pairwise disjoint, and the sets S F i ⊆ [0, 1] n are non-empty and pairwise different2 [START_REF] Boigelot | A generalization of Cobham's theorem to automata over real numbers[END_REF][START_REF] Boigelot | On the sets of real numbers recognized by finite automata in multiple bases[END_REF]. This decomposition of S into sets S I i and S F i is independent from the base r. In addition, each set S I i is recognizable by a finite-word automaton in base r (operating only on the integer part of r-encodings), and each set S F i is (resp. weakly) r-recognizable if S is (resp. weakly) r-recognizable as well [START_REF] Boigelot | A generalization of Cobham's theorem to automata over real numbers[END_REF][START_REF] Boigelot | On the sets of real numbers recognized by finite automata in multiple bases[END_REF].

Consider two multiplicatively independent bases r and s, and a set S ⊆ R n that is both r-and s-recognizable. Applying Semenov's theorem, one obtains that the sets S I i are definable in Z, +, ≤ . It follows that, in order to prove that S is definable in R, Z, +, ≤ , it suffices to show that each set S F i is definable in R, +, ≤, 1 . Since this theory is closed under elimination of quantifiers [START_REF] Ferrante | The Computational Complexity of Logical Theories[END_REF], this is equivalent to proving that each S F i can be expressed as a Boolean combination of linear constraints with rational coefficients.

We have therefore reduced our main problem from R n to the simpler domain [0, 1] n . From now on, we will stay within [0, 1] n and consider that RVA only recognize the fractional part of encodings, their integer part being restricted to zero. Formally, we introduce [w] r , with w ∈ (Σ n r ) ω , as a shorthand for [0 ⋆ w] r .

Reduction to Product-Stable Sets

In order to be able to prove that the recognizability of a subset of [0, 1] n in multiple bases leads to its definability in R, +, ≤, 1 , we need to establish a link between the arithmetical properties of this set, and the structure of automata recognizing it.

Let n ∈ N >0 , r ∈ N >1 , and let S ⊆ [0, 1] n be a set recognized in base r by a RVA A. We associate to each state q of A the language L(q) accepted from q, as well as the set of vectors S(q) ⊆ [0, 1] n encoded by L(q), i.e., S(q

) = {[w] r | w ∈ L(q)}.
Recall that A is a (deterministic) Muller automaton. For each finite path q σ -→ q ′ of A, the language L(q ′ ) can be expressed as

L(q ′ ) = σ -1 L(q) = {w ∈ (Σ n r ) ω | σw ∈ L(q)}.
Similarly, the set S(q ′ ) can be expressed in terms of S(q). Denoting by [σ] r the integer vector encoded by σ, i.e., [σ] r = [0σ ⋆ 0 ω ] r , we get

S(q ′ ) = x ∈ [0, 1] n | [σ] r + x r |σ| ∈ S(q) .
From this relation and Lemmas 1 and 2, one obtains that S(q ′ ) is (resp. weakly) recognizable in all bases for which S(q) is (resp. weakly) recognizable.

Consider now the particular case q = q ′ , i.e., assume that the path labeled by σ cycles from q to itself. The previous relation becomes

x ∈ S(q) ⇔ x ∈ [0, 1] n ∧ [σ] r + x r |σ| ∈ S(q).
Remark that the transformation x → ([σ] r + x)/r |σ| admits the fixed point

x = [σ] r /(r |σ| -1) = [σ ω ] r ∈ [0, 1] n .
Translating S(q) so as to move this fixed point onto 0, one gets

x ∈ S(q) -[σ ω ] r ⇔ x ∈ [0, 1] n -[σ ω ] r ∧ x r |σ| ∈ S(q) -[σ ω ] r .
This prompts the following definition, adapted from [START_REF] Boigelot | On the sets of real numbers recognized by finite automata in multiple bases[END_REF].

Definition 1. Let n ∈ N >0 , v ∈ [0, 1] n ∩ Q n be a pivot, and f ∈ R ≥1 be a factor. A set S ⊆ [0, 1] n is f -product-stable with respect to the pivot v iff ∀x ∈ [0, 1] n -v : x ∈ S -v ⇔ (1/f )x ∈ S -v.
Intuitively, that a set is f -product-stable with respect to the pivot v means that the set does not change when it magnified by the zoom factor f around the fixed point v. Remark that this property is preserved by transformations of the form

x → Cx + a, with C ∈ Q n×n and a ∈ Q n , provided that [0, 1] n ⊆ C[0, 1] n + a, and the new pivot v ′ = Cv + a belongs to [0, 1] n .
In summary, if A recognizes the set S ⊆ [0, 1] n in base r, then each reachable state q of A recognizes a set S(q) ⊆ [0, 1] n that is (resp.weakly) recognizable in all bases for which S is (resp. weakly) recognizable. Furthermore, if there exists a cycle q σ → q, then the set S(q) is r |σ| -product-stable with respect to the pivot [σ ω ] r . We have thus established a link between a structural property of A (the presence of a cycle rooted at q) and an arithmetical property of S(q) (its product stability).

The next step is to show that any recognizable set can be decomposed into a combination of product-stable sets that can be considered individually.

Consider the set Q 1 of states q of A from which there exists a cycle q σ → q, with σ ∈ (Σ n r ) + . Note that every infinite path of A eventually visits a state in Q 1 . Let L be the language of words σ i ∈ (Σ n r ) * labeling finite paths π = q 0 σi → q i such that q 0 is the initial state of A, q i ∈ Q 1 , q ′ ∈ Q 1 for every state q ′ distinct from q i visited by π, and there is only one occurrence of q i in π. The language L is finite, and it maps each σ i ∈ L to a state q i of A. For each such q i , A admits a cycle rooted at q i , hence there exists v i ∈ Q n ∩ [0, 1] n and l i ∈ N >0 such that S(q i ) is r li -product-stable with respect to the pivot v i . Note that each S(q i ) is (resp. weakly) recognizable in all bases for which S is (resp. weakly) recognizable. Moreover, since S = σi∈L (1/r |σi| )(S(q i ) + [σ i ] r ), we have that S is definable in R, +, ≤, 1 if all the sets S(q i ) are definable in the same theory.

It follows from this result that, in order to prove that the recognizability of a set S ⊆ [0, 1] n in multiple bases implies its definability in R, +, ≤, 1 , it is sufficient to prove this property for sets S that are r l -product-stable, with l ∈ N >0 .

Recognizability in Multiple Bases

In this section, we prove the following results, which generalize to R n those developed in [START_REF] Boigelot | A generalization of Cobham's theorem to automata over real numbers[END_REF][START_REF] Boigelot | On the sets of real numbers recognized by finite automata in multiple bases[END_REF].

Theorem 5. Let n ∈ N >0 be a dimension, and r, s ∈ N >1 be bases with different sets of prime factors (i.e., such that there exists a prime factor of one that does not divide the other). If a set S ⊆ [0, 1] n is both r-and s-recognizable, then it is definable in R, +, ≤, 1 . Theorem 6. Let n ∈ N >0 be a dimension, and r, s ∈ N >1 be multiplicatively independent bases. If a set S ⊆ [0, 1] n is both weakly r-and weakly s-recognizable, then it is definable in R, +, ≤, 1 .

Our approach is by induction on n. The case n = 1 is an immediate consequence of [START_REF] Boigelot | A generalization of Cobham's theorem to automata over real numbers[END_REF][START_REF] Boigelot | On the sets of real numbers recognized by finite automata in multiple bases[END_REF]. It remains to address the inductive case where n ≥ 2, assuming that Theorems 5 and 6 hold for smaller dimensions. Exploiting the results of Section 3.2, we only consider w.l.o.g. sets S ⊆ [0, 1] n that are r l -product-stable for some l ∈ N >0 and pivot v ∈ [0, 1] n ∩ Q n .

Using s-recognizability

Consider a set S ⊆ [0, 1] n that is recognizable in two bases r, s ∈ N >1 . Assume that there exist l ∈ N >0 and v ∈ [0, 1] n ∩ Q n such that S is r l -product-stable with respect to the pivot v. We show in this section that there exists an integer l ′ ∈ N >0 such that S is s l ′ -product-stable as well.

We first consider the case v = 0. Let A s be a RVA recognizing S in base s. We assume w.l.o.g. that A s has a complete transition relation, hence it admits an ultimately cyclic path labeled by 0 ω , which we denote

q 0 0 m -→ [q 0 l ′ -→] ω ,
where q 0 is the initial state of A s , m ∈ N and l ′ ∈ N >0 . By the same reasoning as in Section 3.2, we obtain that the set S(q) encoded in base s by the language L(q) accepted from q in A s is both r-and s-recognizable. Moreover, S(q) is s l ′ -product-stable with respect to the pivot 0.

Since A s is deterministic, it admits only one path from q 0 to q labeled by 0 m , which leads to S(q) = s m S ∩ [0, 1] n . From this relation, and the r l -productstability hypothesis on S, it follows that S(q) is r l -product-stable as well, with respect to the pivot 0.

The set S(q) is thus both r l -and s l ′ -product-stable, with respect to the same pivot 0. Let us show that these properties imply that S itself is both r l -and s l ′ -product-stable. By hypothesis, S is r l -product-stable with respect to 0. For any x ∈ [0, 1] n and k ∈ N, we thus obtain

x ∈ S ⇔ 1 r lk x ∈ S ⇔ s |σ ′ | r lk x ∈ s |σ ′ | S ⇔ s |σ ′ | r lk x ∈ S(q),
if k is chosen large enough to have r lk ≥ s |σ ′ | . Since S(q) is s l ′ -product-stable with respect to 0, we get

s |σ ′ | r lk x ∈ S(q) ⇔ s |σ ′ |-l ′ r lk x ∈ S(q) ⇔ 1 r lk s l ′ x ∈ S ⇔ 1 s l ′ x ∈ S.
proving that S is s l ′ -product-stable with respect to v in the special case v = 0.

The general case v ∈ [0, 1] n ∩ Q n is obtained by decomposing S according to the 2 n possible positions of vectors in [0, 1] n with respect to v. For each vector a ∈ {-1, 1} n we introduce the matrix M a = diag(a), the set

D a = (v + M a R n ≥0 ) ∩ [0, 1] n and the set S a = S ∩ D a . Each set D a is a Cartesian product of intervals D a = I 1 × • • • × I n ,
where for all i ∈ {1, . . . , n},

I i = [v i , 1] if a i = 1, [0, v i ] if a i = -1.
The vectors a such that D a has a positive volume are identified by introducing the set A of vectors a such that f i (v i ) > 0 for any i ∈ {1, . . . , n}, where f i (v i ) denotes the length of the interval I i , i.e

f i (v i ) = 1 -v i if a i = 1, v i if a i = -1.
Since each zero volume set is included into at least one positive volume set, we have a∈A D a = [0, 1] n , which implies S = a∈A S a .

For each a ∈ A, the set M a (D av) takes the form of the Cartesian product [0,

f 1 (v 1 )] × • • • × [0, f n (v n )].
We can thus map the elements of D a onto [0, 1] n by defining the transformation x → C a M a (xv), where C a = diag(1/f 1 (v 1 ), . . . ,

1/f n (v n )).
We now consider, for each a ∈ A, the set S ′ a = C a M a (S av). From the r l -product-stability of S with respect to v, it follows that S ′ a is r l -product-stable with respect to 0. By Lemmas 1 and 2, S ′ a inherits the recognizability properties of S. Moreover, there exists l ′ a ∈ N >0 such that S ′ a is s l ′ a -product-stable with respect to 0. From this property and the equality S a = v + M -1 a C -1 a S a , we deduce that S a is s l ′ a -product-stable with respect to v. From S = a∈A S a , it then follows that S is s l ′ -product-stable, where l ′ = lcm a∈A (l ′ a ). In summary, we have established that S, in addition to being r l -productstable by hypothesis, is s l ′ -product-stable as well. It remains to show that these properties, combined with our inductive hypotheses, imply that S is definable in R, +, ≤, 1 .

Exploiting Multiple Product Stabilities

We thus consider a set S ⊆ [0, 1] n and two bases r, s ∈ N >1 , such that either r and s are multiplicatively independent and S is weakly r-and weakly s-recognizable, or r and s do not share the same set of prime factors3 and S is r-and srecognizable. Using the results of Section 4.1, we assume that there exist l, l ′ ∈ N >0 and v ∈ [0, 1] n ∩ Q n such that S is both r l -and s l ′ -product-stable with respect to the pivot v. Our goal is to show that S is definable in R, +, ≤, 1 .

We first prove the following property.

Property 1. For each x ∈ [0, 1] n ∩ Q n such that x = v, let h v (x) denote the set {v + λ(x -v) ∈ [0, 1] n | λ ∈ R >0 }. We have either h v (x) ⊆ S, or h v (x) ∩ S = ∅. Proof sketch. Consider x ∈ [0, 1] n ∩ Q n such that x = v.
The set h v (x) can be expressed as an intersection of linear inequalities with rational coefficients, and is thus weakly recognizable in all bases, as a consequence of Theorems 1 and 2.

From Lemma 1, it follows that the set S ′ = S ∩ h v (x) is recognizable both in bases r and s, by the same type of automaton as S. Besides, S ′ is both r l -and s l ′ -product-stable with respect to the pivot v.

Let C ∈ Q n×n be a non-singular matrix such that C(xv) = (1, 0, . . . , 0). Note that the transformation y → Cy maps h v (x) onto a line segment that is parallel to the first axis. From Lemmas 1 and 2, we have that the set S ′′ = C(S ′v) ∩ [0, 1] n inherits the recognizability properties of S. Moreover, S ′′ is r l -and s l ′ -product-stable with respect to the pivot 0.

Note that the set S ′′ can be decomposed into S ′′ = S ′′′ × {0} n-1 , with S ′′′ ⊆ [0, 1]. Applying Lemma 3, the set S ′′′ has the same recognizability properties as S hence, by the inductive hypotheses, it is definable in R, +, ≤, 1 . In other words, S ′′′ is equal to a finite union of intervals with rational boundaries.

In addition, we know that S ′′′ is r l -and s l ′ -product-stable with respect to the pivot 0. Since r and s are multiplicatively independent, r l and s l ′ are multiplicatively independent as well. By Kronecker's approximation lemma, the set {r li s l ′ j ∈]0, 1] | i, j ∈ Z} is dense in ]0, 1], as shown in [START_REF] Hardy | An introduction to the theory of numbers[END_REF][START_REF] Boigelot | On the sets of real numbers recognized by finite automata in multiple bases[END_REF]. It follows that if 1 ∈ S ′′′ then S ′′′ \ {0} =]0, 1] and if 1 ∈ S ′′′ then S ′′′ \ {0} = ∅. As a consequence, h v (x) ∩ S is either empty, or equal to h v (x).

⊓ ⊔ Intuitively, Property 1 hints at the fact that the set S has a conical structure. We formalize this property by the following definition.

Definition 2. A set T ⊆ [0, 1] n is a conical set of vertex v ∈ [0, 1] n iff ∀x ∈ [0, 1] n , f ∈]0, 1] : x ∈ T ⇔ f (x -v) + v ∈ T .
In other words, a conical set is entirely determined by its vertex, and its intersection with the faces of the hypercube [0, 1] n . It follows that, in order to establish that S is definable in R, +, ≤, 1 , it suffices to show that this intersection is definable in the same theory, and that S is a conical set. We have the following results. Property 2. For each i ∈ {1, 2, . . . , n} and λ ∈ {0, 1}, let

F λ,i = {x ∈ [0, 1] n | x i = λ}. The set S ∩ F λ,i is definable in R, +, ≤, 1 .
Proof sketch. Let i ∈ {1, 2, . . . , n} and λ ∈ {0, 1}. We first build the permutation matrix C ∈ {0, 1} n×n such that Cx = (x 1 , . . . , x i-1 , x i+1 , . . . , x n , x i ) for any x = (x 1 , . . . , x n ) ∈ R n . The set F λ,i is definable in R, +, ≤, 1 , hence it is weakly r-recognizable. From Lemmas 1 and 2, the set S ′ = C(S ∩ F λ,i ) inherits the recognizability properties of S. Moreover, we have S ′ = S ′′ × {λ}, where S ′′ ⊆ [0, 1] n-1 has the same recognizability properties as well, as a consequence of Lemma 3. The result then follows from the inductive hypotheses.

⊓ ⊔ Property 3. The set S is conical with respect to the vertex v.

Proof sketch. Let S ′ be the intersection of S with the faces of the hypercube [0, 1] n . We have established that S ′ is definable in R, +, ≤, 1 . The set S ′ can thus be expressed as a finite Boolean combination of linear constraints with rational coefficients. As a consequence, there exists a set S ′′ ⊆ [0, 1] n that is definable in R, +, ≤, 1 , conical with respect to the vertex v, and that coincides with S ′ over the faces of [0, 1] n and over the vertex v. Applying Property 1, we obtain S ′′ ∩ Q n = S ∩ Q n . From Theorem 4, we then have S = S ′′ . ⊓ ⊔

Internal Structure of RVA

In Section 4, we have proved Theorems 5 and 6, which broadly state that if a set S ⊆ [0, 1] n is recognizable or weakly recognizable in two bases r and s that are sufficiently different, then this set is definable in R, +, ≤, 1 . As a corollary, such sets are then weakly recognizable in every base r ∈ N >1 [START_REF] Boigelot | An effective decision procedure for linear arithmetic over the integers and reals[END_REF]. This result is significant, since it establishes that the class of weak deterministic automata is sufficient for representing all the sets that are recognizable by RVA regardless of the numeration base. As mentioned earlier, the advantage of using weak deterministic automata in actual applications comes from the fact that these automata are basically as easy to handle algorithmically as finite-word ones [START_REF] Wilke | Locally threshold testable languages of infinite words[END_REF]. We now use Theorems 5 and 6, together with other results obtained in Section 4, in order to get some insight into the internal structure of RVA recognizing the subsets of [0, 1] n definable in R, +, ≤, 1 . As explained in Section 3, this is equivalent to studying the structure of RVA recognizing sets definable in R, Z, +, ≤ , staying within the part of automata that reads the fractional part of vectors (i.e., in the sub-automata whose initial states are the destinations of transitions labeled by "⋆").

Let n ∈ N >0 be a dimension, r ∈ N >1 be a base, and S ⊆ [0, 1] n be a set definable in R, +, ≤, 1 . We consider a weak and deterministic RVA A recognizing S in base r. We assume w.l.o.g. that A is complete as well as minimal (in the sense of [START_REF] Löding | Efficient minimization of deterministic weak ω-automata[END_REF]).

As observed in Section 3.2, for each state q of A, the set S(q) ⊆ [0, 1] n encoded by the language L(q) accepted from q can be derived from S by a transformation that is definable in R, +, ≤, 1 . It follows that each S(q) is itself definable in that theory.

In addition, it has been established in Section 4.2 that, for the states q that belong to non-trivial strongly connected components of A (i.e., such that there exists at least one cycle from q to itself), the set S(q) is a conical set. It is however worth noticing that the vertex of this conical set may not be uniquely determined. For instance, every element of the conical set {(0, λ) | λ ∈ [0, 1]} is one of its vertices. We have the following result.

Theorem 7. Let n ∈ N >0 , and T ⊆ [0, 1] n be a conical set. The vertices of T form a bounded affine space {v

+ ν 1 u 1 + • • • + ν m u m ∈ [0, 1] n | ν 1 , . . . , ν m ∈ R}, with m ∈ N and v, u 1 , . . . , u m ∈ R n . Proof sketch. It is sufficient to prove that, if v 1 , v 2 ∈ [0, 1] n are two distinct vertices of T , then each point on the line segment L = {µv 1 +(1-µ)v 2 ∈ [0, 1] n | µ ∈ R } linking v 1 and v 2 is
also a vertex of T . This can be achieved by showing that T is invariant under any translation parallel to L that stays within [0, 1] n , i.e., that

x ∈ T ⇔ x + µ(v 1 -v 2 ) ∈ T for all x ∈ [0, 1] n and µ ∈ R such that x + µ(v 1 -v 2 ) ∈ [0, 1] n .
Let x be an arbitrary vector in [0, 1] n . Consider an arbitrary value µ ∈ R ≥0 such that x + µ(v 1v 2 ) ∈ [0, 1] n . (Note that restricting µ to be non negative does not weaken the property.)

We define

x ′ = x + µ(v 1 -v 2 ) and f = 1/(1 + µ). Since T is a conical set w.r.t. the vertex v 1 , we have x ∈ T if and only if f (x -v 1 ) + v 1 ∈ T . Exploiting the conical structure of T w.r.t. the vertex v 2 , we then get x ′ ∈ T if and only if f (x ′ -v 2 ) + v 2 ∈ T . By replacing x ′ by x + µ(v 1 -v 2 ) we deduce the equality f (x ′ -v 2 ) + v 2 = f (x -v 1 ) + v 1 which yields x ∈ T ⇔ x ′ ∈ T .
⊓ ⊔ We are now ready to describe the structure of A: Its initial state is the root of a (possibly empty) acyclic structure, composed of states belonging to trivial strongly connected components, and leading to states q belonging to non-trivial components. For each such state q, the set S(q) ⊆ [0, 1] n is conical. Such a set is entirely characterized by the affine space containing its vertices, a Boolean value stating whether these vertices belong or not to S(q), and the intersection of the set with the 2n faces of the hypercube [0, 1] n . This intersection can be expressed in terms of at most 2n subsets of [0, 1] n-1 (in the bottom case n = 1, this degenerates into the two extremities of the interval [0, 1]), which are known to be recognizable in R, +, ≤, 1 .

Those observations could lead to a more efficient data structure for representing canonically the subsets of [0, 1] n that are definable in additive arithmetic. For instance, RVA could be represented implicitly, by using BDDs for describing their initial acyclic structure [START_REF] Bryant | Symbolic Boolean manipulation with ordered binary decision diagrams[END_REF] and linking this structure to representations of conical sets. These sets could be described by encoding separately the affine space containing their vertices and the faces of their enclosing hypercube. These faces could themselves be represented by the same type of structure applied to subsets of [0, 1] n-1 . The bottom layer of such a hierarchical representation would correspond to individual rational numbers, which could be encoded explicitly.

The detailed study of such a representation system, and its application to decision procedures for R, +, ≤, 1 and R, Z, +, ≤ , will be the subject of future work.

Conclusions

In this paper, we have characterized the subsets of R n , with n ∈ N >0 , that are recognizable by RVA, or weak deterministic RVA, in multiple bases. Precisely, we have established that the sets that are either weakly recognizable in two multiplicatively independent bases, or recognizable in two bases that do not share the same set of prime factors, are exactly those that are definable in the first-order theory R, Z, +, ≤ . These results were already known for the particular case n = 1 [START_REF] Boigelot | A generalization of Cobham's theorem to automata over real numbers[END_REF][START_REF] Boigelot | On the sets of real numbers recognized by finite automata in multiple bases[END_REF]. They generalize to automata operating on real vectors Semenov's theorem, which states that the sets of integer vector that are recognizable in multiplicatively independent bases are those that are definable in Presburger arithmetic. The theory R, Z, +, ≤ can indeed be seen as an extension of Presburger arithmetic to mixed integer and real variables [START_REF] Weispfenning | Mixed real-integer linear quantifier elimination[END_REF]. It is worth mentioning that, in the case of (non weak) recognizability, the condition on the numeration bases cannot be replaced by multiplicative independence. Indeed, there exist subsets of R that are simultaneously recognizable in two multiplicatively independent bases, but without being definable in additive arithmetic [START_REF] Boigelot | On the sets of real numbers recognized by finite automata in multiple bases[END_REF].

An important corollary of our results is that every subset of R n that is recognizable in every base r ∈ N >1 can be recognized by a weak deterministic automaton. This provides a theoretical justification to the use of these automata for representing sets of integer and real vectors, in addition to their practical advantages.

As an additional contribution, we have obtained interesting insight into the structure of weak deterministic automata recognizing sets definable in the theory R, Z, +, ≤ . In future work, we will address the problem of exploiting this structure in order to develop more efficient symbolic representation systems for subsets of R n , as well as an improved decision procedure for R, Z, +, ≤ . Our aim is to be able to benefit from the advantages of automata-based symbolic representations, which mainly reside in their easy algorithmic manipulation and their canonicity, while managing to avoid some of their drawbacks, such as the unnecessarily large size of automata obtained from some classes of constraints [START_REF] Eisinger | Don't care words with an application to the automatabased approach for real addition[END_REF]. This could be achievable by keeping a part of the transition relation of RVA implicit. Such a representation would also simplify the problem of extracting formulas from automata recognizing arithmetic sets [START_REF] Latour | Presburger arithmetic: from automata to formulas[END_REF][START_REF] Leroux | A polynomial time Presburger criterion and synthesis for number decision diagrams[END_REF].

As opposed to the integer case, it has been shown that the result does not hold for multiplicatively independent bases[START_REF] Boigelot | On the sets of real numbers recognized by finite automata in multiple bases[END_REF].

The property is actually known for the domain R, but straightforwardly generalizes to R n .

Note that this constraint implies that r and s are multiplicatively independent.

⋆ This work is supported by the Interuniversity Attraction Poles program MoVES of the Belgian Federal Science Policy Office, by the grant 2.4530.02 of the Belgian Fund for Scientific Research (F.R.S.-FNRS), and by the French project ANR-06-SETI-001 AVERISS. ⋆⋆ Research fellow ("Aspirant") of the Belgian Fund for Scientific Research (F.R.S.-FNRS).