key: cord-0060371-sc9ijntp
authors: Haase, Christoph; Różycki, Jakub
title: On the Expressiveness of Büchi Arithmetic
date: 2021-03-23
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-71995-1_16
sha: 7bd7b6ed65f5c2e2545ef378e1f037afdb616631
doc_id: 60371
cord_uid: sc9ijntp

We show that the existential fragment of Büchi arithmetic is strictly less expressive than full Büchi arithmetic of any base, and moreover establish that its [Formula: see text] -fragment is already expressively complete. Furthermore, we show that regular languages of polynomial growth are definable in the existential fragment of Büchi arithmetic.

This paper studies the expressive power of Büchi arithmetic, an extension of Presburger arithmetic, the first-order theory of the structure N, 0, 1, + . Büchi arithmetic additionally allows for expressing restricted divisibility properties while retaining decidability. Given an integer p ≥ 2, Büchi arithmetic of base p is the first-order theory of the structure N, 0, 1, +, V p , where V p is a binary predicate such that V p (a, b) holds if and only if a is the largest power of p dividing b without remainder, i.e., a = p k , a | b and p · a b.

Presburger arithmetic admits quantifier-elimination in the extended structure N, 0, 1, +, {c|·} c>1 additionally consisting of unary divisibility predicates c|· for every c > 1 [10] . It follows that the existential fragment of Presburger arithmetic is expressively complete, since any predicate c|· can be expressed using an additional existentially quantified variable. We study the analogous question for Büchi arithmetic and show, as the main result of this paper, that its existential fragment is, in any base, strictly less expressive than full Büchi arithmetic. Notably, this result implies that there does not exist a quantifierelimination resultà la Presburger for Büchi arithmetic, i.e., any extension of Büchi arithmetic with additional predicates definable in existential Büchi arithmetic does not admit quantifier elimination.

A central result about Büchi arithmetic is that it is an automatic structure: a set M ⊆ N n is definable in Büchi arithmetic of base p if and only if M is recognizable by a finite-state automaton under a base p encoding of the natural numbers. Equivalently, M is p-regular. This result was first stated by Büchi [4] , albeit in an incorrect form, and later correctly stated and proved by Bruyère [2] , see also [3] . Villemaire showed that the Σ 3 -fragment of Büchi arithmetic is expressively complete [13, Cor. 2.4] . He established this result by showing how to construct a Σ 3 -formula defining the language of a given finite-state automaton. We observe that Villemaire's construction can actually be improved to a Σ 2formula and thus obtain a full characterization of the expressive power of Büchi arithmetic in terms of the number of quantifier alternations.

Our approach to separating the expressiveness of existential Büchi arithmetic from full Büchi arithmetic in base p is based on a counting argument. Given a set M ⊆ N, define the counting function d M (n) := #(M ∩ {p n−1 , . . . , p n − 1}) which counts the numbers of bit-length n in base p in M . If M is definable in existential Büchi arithmetic of base p, we show that d M is either O(n c ) for some c ≥ 0, or at least c · p n for some constant c > 0 and infinitely many n ∈ N. Since, for instance, for M p ⊆ N defined as the set of numbers with p-ary expansion in the regular language {10, 01} * , we have d Mp (n) = Θ(2 n/2 ), and hence M p is not definable in existential Büchi arithmetic of base p. However, M p being p-regular implies that M p is definable by a Σ 2 -formula of Büchi arithmetic of base p.

We also show that existential Büchi arithmetic defines all regular languages of polynomial density, encoded as sets of integers. Given a language L ⊆ Σ * , let the counting function d L : N → N be such that d L (n) := #(L ∩ Σ n ). Szilard et al. [11] say that L has polynomial density whenever d L (n) is O(n c ) for some non-negative integer c. If moreover L is regular then Szilard et al. show that L is represented as a finite union of regular expressions of the form v 0 w * [11, Thm. 3] . We show that existential Büchi arithmetic defines any language represented by a regular expression v 0 w * 1 v 1 · · · w * k v k , which implies that existential Büchi arithmetic defines all regular languages of polynomial density.

Let Σ be an alphabet and w ∈ Σ * , we denote by |w| the length of w. Given a set U ⊆ N, we denote by w U := {w u : u ∈ U }. Thus, for example, w * = w N .

For an integer p ≥ 2, let Σ p := {0, . . . , p − 1}. We view words over Σ p as numbers encoded in p-ary most-significant bit first encoding. Tuples of numbers of dimension n can be encoded as words over the alphabet Σ n p . For w = v m · · · v 0 ∈ (Σ n p ) m+1 , we denote by w p ∈ N n the n-tuple

We furthermore define ε p := 0. Note that · p is not injective since, e.g., 01 and 001 both encode the number one. Given L ⊆ (Σ n p ) * , we define

is the transition function, q 0 ∈ Q is the initial state, and -F ⊆ Q is the set of final states.

For states q, r ∈ Q and u ∈ Σ, we write q u − → r if δ(q, u) = r, and extend − → inductively to words by stipulating, for w ∈ Σ * and u ∈ Σ, that q

Note that a priori we allow automata to have infinitely many states and to have partially defined transition functions (due to the presence of ⊥ in the co-domain of δ). If Q is finite then we call A a deterministic finite automaton (DFA), and if in addition Σ = Σ n p for some p ≥ 2 and n ≥ 1 then A is called a p-automaton. Throughout this paper, we assume, without loss of generality, that all states of a DFA are live, i.e., every state is reachable from the initial state and can reach an accepting state.

Arithmetic theories. As stated in the introduction, Presburger arithmetic is the first-order theory of the structure N, 0, 1, + , and Büchi arithmetic of base p the first-order theory of the extended structure N, 0, 1, +, V p . We write atomic formulas of Presburger arithmetic as a · x = c, where a = (a 1 , . . . , a d ) with a i ∈ Z, c ∈ Z, and x = (x 1 , . . . , x d ) is a vector of unknowns. In Büchi arithmetic we additionally have atomic formulas V p (x, y) for the unknowns x and y. For technical convenience, we assert that V p (x, 0) never holds. 3 We write Φ(x) or Φ(x) to indicate that x or a vector of unknowns x occurs free in Φ. If there are further free variables in Φ, we assume them to be implicitly existentially quantified.

We may without loss of generality assume that no negation symbol occurs in a formula of Büchi arithmetic. First, we have ¬(a · x = c) ≡ a · x ≤ c − 1 ∨ a · x ≥ c + 1, and the order relation ≤ can easily be expressed by introducing an additionally existentially quantified variable. Moreover, we have

Finally, P p (x) := V p (x, x) denotes the macro asserting that x is a power of p.

Given a formula Φ(x) of Büchi arithmetic of base p, we define 3 Other conventions are possible, e.g., asserting that Vp(x, 0) holds if and only if x = 1 as in [3] , but this does not change the sets of numbers definable in Büchi arithmetic.

where, for m = (m 1 , . . . , m d ) and x = (x 1 , . . . , x d ), Φ[m/x] is the formula obtained from replacing every x i by m i in Φ. The set of sets of numbers definable in Presburger arithmetic is denoted by

Analogously, we define the sets of numbers definable in fragments of Büchi arithmetic of base p with a fixed number of quantifier-alternations as

Finally, BA p := i≥1 Σ i -BA p denotes the sets of numbers definable in Büchi arithmetic of base p.

For separating existential Büchi arithmetic from full Büchi arithmetic, we employ some tools from enumerative combinatorics. As defined in [15], a formula of parametric Presburger arithmetic with parameter t is a formula of Presburger arithmetic Φ t in which atomic formulas are of the form a · x = c(t), where c(t) is a univariate polynomial with indeterminate t and coefficients in Z. For n ∈ N, we denote by Φ n the formula of Presburger arithmetic obtained from replacing c(t) in every atomic formula of Φ t by the value of c(n). We associate to a formula

Throughout this paper, we constraint ourselves to formulas Φ t (x) of parametric Presburger arithmetic in which c(t) is the identity function and #Φ t (x)(n) is finite for all n ∈ N.

Given an eventual quasi-polynomial f with threshold t and n > t, we denote by f n the polynomial p i such that n ≡ i mod m. We say that the polynomials p 0 , . . . , p m−1 constitute the eventual quasi-polynomial f . A result by Woods [15, Thm. 3.5(b)] shows that the counting functions associated to parametric Presburger formulas as defined above are eventual quasi-polynomial.

Semi-linear sets. A result by Ginsburg and Spanier establishes that the sets of numbers definable in Presburger arithmetic are semi-linear sets [7] . A linear set in dimension d is given by a base vector b ∈ N d and a finite set of period vectors P = {p 1 , . . . , p n } ⊆ N d and defines the set

A semi-linear set is a finite union of linear sets. For a finite B ⊆ N d , we write L(B, P ) for b∈B L(b, P ). Semi-linear sets of the form L(B, P ) are called hybrid linear sets in [5] , and it is known that the set of non-negative integer solutions of a system of linear Diophantine inequalities S : A · x ≥ c is a hybrid linear set [5] .

Semi-linear sets in dimension one are also known as ultimately periodic sets. In this paper, we represent an ultimately periodic set as a four-tuple U = (t, , B, R), where t ≥ 0 is a threshold, > 0 is a period, B ⊆ {0, . . . , t − 1} and R ⊆ {0, . . . , − 1}, and U defines the set

We now establish the main result of this paper and show that the existential fragment of Büchi arithmetic is strictly less expressive than general Büchi arithmetic.

Given a set M ⊆ N, recall that for a fixed base p ≥ 2, d M (n) counts the numbers of bit-length n in base p in M . As already discussed in the introduction, we prove Theorem 1 by characterizing the growth of d M for sets M definable in Büchi arithmetic.

For any formula Φ(x) of existential Büchi arithmetic in prenex normal form, we can with no loss of generality assume that its matrix is in disjunctive normal form, i.e., a disjunction of systems of linear Diophantine equations with valuation constraints, each of the form

where the x i and y i are unknowns from the vector of unknowns x. For M = Φ(x) p , in order to determine the growth of d M , it suffices to determine the maximum growth occurring in any of its systems of linear Diophantine equations with valuation constraints in the matrix of Φ(x), which in turn can be obtained by analyzing the growth of the number of words accepted by a p-automaton defining the set of solutions of such a system. Let S : A · x = c be a system of linear Diophantine equations such that, throughout this section, A is an m × d integer matrix, and fix a base p ≥ 2. Following Wolper and Boigelot [14] , we define an automaton A := (Q, Σ d p , δ, q 0 , F ) whose language encodes all solutions of S over the alphabet Σ p :

As discussed in [14] , see also [8] , only states q such that q ∞ ≤ A 1,∞ and q ∞ ≤ c ∞ can reach the accepting state. Hence, all words w ∈ (Σ d p ) * such that A · w = c only visit a finite number of states of A, and to obtain the p-automaton A(S) defining the sets of solutions of S we subsequently restrict Q to only such states. The following lemma recalls an algebraic characterization of the reachability relation of A(S) established in the proof of Proposition 14 in [8] .

Lemma 1. Let q, r ∈ Z m be states of A(S), w ∈ (Σ d p ) n and x = w p . Then q w − → r if and only if there is y ∈ N such that q = r · y + A · x, x ∞ < y, y = p n .

Let x be a distinguished variable of x. For a word w ∈ (Σ d p ) * encoding solutions of S, denote by π x (w) the word v ∈ Σ * p obtained from projecting w onto the component of w corresponding to x. Let q be a state of a p-automaton A, define the counting function C q,x : N → N as

We now show that for p-automata arising from systems of linear Diophantine equations, C q,x can be obtained from an eventual quasi-polynomial.

Lemma 2. For the p-automaton A(S) associated to S : A · x = c with states Q and all q ∈ Q, there is an eventual quasi-polynomial f such that C q,x (n) = f (p n ) for all n ∈ N. Moreover, for all sufficiently large n ∈ N, f p n is a linear polynomial.

Proof. Let q = q ∈ Z d . By Lemma 1, q w − → q for w ∈ (Σ d p ) n if and only if there is a y ∈ N such that q = q · y + A · x, x ∞ < y, y = p n , where x = w p . The set of solutions of S : A · x + q · y = q, x ∞ < y is a hybrid linear set L(D, R) ⊆ N d+1 . Let L(B, P ) ⊆ N 2 be obtained from L(D, R) by projecting onto the components corresponding to x and y, and assume that Observe that C q,x (n) = f (p n ) and that f (n) is finite for all n ∈ N due to the constraint x < y. Let P = {p 1 , . . . , p k }, the following formula of parametric Presburger arithmetic defines L(B, P ) ∩ M t :

Thus, f = #Φ t (x, y) and, by application of Proposition 1, f is an eventual quasi-polynomial. Since C q,x (n) ≤ p n −1 for all n ∈ N, we in particular have that all polynomials f p n constituting f are linear as they would otherwise outgrow C q,x . The next step is to lift Lemma 2 to systems of linear Diophantine equations with valuation constraints. To this end, we define a DFA whose language encodes the set of all solutions of predicates of the form V p (x, y). Formally, for S : V p (x, y) we define A(S) := (Q, Σ d p , δ, q 0 , F ) such that -Q := {0, 1}, δ(0, u) := 0 for all u ∈ Σ d p such that π x (u) = 0, δ(0, u) := 1 for all u ∈ Σ d p such that π x (u) = 1 and π y (u) > 0, δ(1, u) := 1 for all u ∈ Σ d p such that π x (u) = π y (u) = 0, q 0 := 0, and -F := {1}.

For S : A · x = c ∧ 1≤i≤ V p (x i , y i ), we denote by A(S) the DFA that can be obtained from the standard product construction on all DFA for the atomic formulas of S. Hence, the set of states of A(S) is a finite subset of Z m ×{0, 1} . We now show that the number of words along a cycle of A(S) can also be obtained from an eventual quasi-polynomial.

Lemma 3. Let S be a system of linear Diophantine equations with valuation constraints with the associated DFA A(S) with states Q, and let q ∈ Q. There is an eventual quasi-polynomial f such that C q,x (n) = f (p n ). Moreover, f p n is a linear polynomial for all n ∈ N.

and thus q = (q, b 1 , . . . , b ) ∈ Q. Any self-loop q w − → S q with q = (q, b 1 , . . . , b ) is a self-loop for the DFA induced by the system of linear Diophantine equations A · x = c with the additional requirement that π xi ( w p ) = 0 for all 1 ≤ i ≤ and furthermore π yi ( w p ) = 0 whenever b i = 1. Thus (q, 0)

Conversely, (q, 0) w − → S (q, 0) immediately gives q w − → S q. The statement is now an immediate consequence of the application of Lemma 2 to S .

We will from now on implicitly apply Lemma 3. As a first application, we show that Lemma 3 allows us to classify the DFA associated to a system of linear Diophantine equations with valuation constraints. (i) there is q ∈ Q such that C q,x is an eventual quasi-polynomial f and f p n is a non-constant polynomial for infinitely many n ∈ N; or (ii) there is a constant d ≥ 0 such that C q,x (n) ≤ d for all q ∈ Q and n ∈ N.

Proof. Suppose A(S) has Property (i). For a contradiction, suppose d ≥ 0 exists. Let f be the eventual quasi-polynomial from Property (i). Every non-constant polynomial f p n constituting f is of the form a · x + b with a > 0. As there are infinitely many such n, there is some linear polynomial g(x) = a · x + b such that g = f p n for infinitely many n ∈ N. Hence g(p n ) > d for some sufficiently large n ∈ N.

For the converse, suppose that A(S) does not have Property (i). Then there are , m > 0 such that all f p n are constant polynomials bounded by some value m ∈ N for all n ≥ , q ∈ Q and f = C q,x . Hence we can choose d = max({C q,x (n) : q ∈ Q, 0 < n ≤ } ∪ {m}).

We are now in a position to prove a dichotomy of the growth of the number of words accepted by a DFA corresponding to a system of linear Diophantine equations with valuation constraints. If A(S) has the Property (i) of Lemma 4 then consider q ∈ Q such that C q,x is an eventual quasi-polynomial f such that f p n is non-constant for infinitely many n ∈ N, and let i 1 < i 2 < . . . ∈ N be such that all f p i j are the same non-constant polynomial a · x + b. Consider v and w such that q 0 v − → q w − → q f . Then for all sufficiently large j we have

for some fixed constant c > 0.

Otherwise, A(S) has the Property (ii) of Lemma 4, and there is some fixed d ≥ 0 such that C q,x (n) ≤ d for all n ∈ N and q ∈ Q. Every w ∈ L such that |w| = n can uniquely be decomposed as w = v 0 w 1 v 1 w 2 · · · w k v k for some k ≤ |Q| such that

where q a k+1 = q f , q ai = q aj for all i = j and each q ai vi − → q ai+1 corresponds to a loop-free path in A(S). Since C q,x ≤ d, there are at most d k ≤ d (#Q) words u ∈ L of length n that have the same sequence of states in the decomposition of Eq. (1) at the same position where they occur in w. Moreover, there are at most n 2k ≤ n 2·#Q ≤ n (2·#Q) possibilities at which the states q ai can appear in any u ∈ L of length n for any particular sequence of states in the decomposition of Eq. (1). Finally, there are at most (#Q) (#Q) such sequences. We thus derive

for some constant c ≥ 0. Corollary 1. Let Φ(x) be a fixed formula of existential Büchi arithmetic of base p ≥ 2. Let M = Φ(x) p , then either:

(i) d M (n) ≥ c · p n for some fixed constant c > 0 and infinitely many n ∈ N; or (ii) d M (n) = O(n c ) for some fixed constant c ≥ 0.

Proof. Without loss of generality we may assume that Φ(x) is in disjunctive normal form such that Φ(x) = i∈I Φ i (x) and each Φ i (x) is a system of linear Diophantine equations with valuation constraints S i . For M i = Φ i (x) p , we obtain d Mi by application of Lemma 5. If there is a constant c ≥ 0 such that d Mi = O(n c ) for all i ∈ I then d M = O(n c ). Otherwise, if there is some i ∈ I such that d Mi (n) ≥ c · p n for some constant c > 0 and infinitely many n ∈ N then d M (n) ≥ c · p n for infinitely many n ∈ N.

As an immediate consequence of Corollary 1, we obtain:

For any p ≥ 2, consider L = {01, 10} * ⊆ Σ * p and M = L p . We have d M (n) = Θ(2 n/2 ), and thus Corollary 2 yields M ∈ Σ 1 -BA p . However, since M is pregular, we have M ∈ BA p . This concludes the proof of Theorem 1.

For a regular language L ⊆ (Σ d p ) * given by a DFA, Villemaire shows in the proof of Theorem 2.2 in [13] how to construct a Σ 3 -formula of Büchi arithmetic Φ L (x) such that Φ L (x) p = L p . This construction is modularized and relies on an existential formula Φ p,j (x, y) expressing that "x is a power of p and the coefficient of this power of p in the representation of y in base p is j":

The only reason why Φ L (x) in [13] is a Σ 3 -formula is that Φ p,j (x, y) appears in an implication both as antecedent and as consequent inside an existential formula. Thus, if one could additionally define Φ p,j (x, y) by a Π 1 -formula then Φ L (x) immediately becomes a Σ 2 -formula. That is, however, not difficult to achieve by defining:

Φ p,j (x, y) := P p (x) ∧ ∀s ∀t ∀u ∀z :

Note that the order relation can also be expressed by a universal formula: x ≤ y if and only if ∀z : (y + z = x) → (z = 0). Thus, Φ p,j (x, y) is indeed a Π 1 formula.

Combining Φ p,j (x, y) with the results in [13] , we obtain that the Σ 2 -fragment of Büchi arithmetic is expressively complete.

Theorem 2. For any base p ≥ 2, Σ 2 -BA p = BA p .

For a language L ⊆ Σ * , Szilard et al. [11] say that L has polynomial growth if d L (n) = O(n c ) for some constant c ≥ 0 and all n ∈ N. One of the main results of [11] is that a regular language L has polynomial growth if and only if L can be represented as a finite union of regular expressions of the form

Denote by PREG p := L p : L ⊆ Σ * p , L is a regular language of polynomial growth the numerical encoding of all regular languages of polynomial growth in base p. We show in this section that existential Büchi arithmetic defines any regular language of the form in Eq. (2) . This immediately gives the following theorem.

Theorem 3. For any base p ≥ 2, PREG p ⊆ Σ 1 -BA p .

We first require a couple of abbreviations. Define

which expresses that y is the smallest power of p strictly greater than x. Let > 0, Lohrey and Zetzsche introduce in [9] the predicate S (x, y) which holds whenever x = p r and y = p r+ ·i for some i, r ≥ 0 .

They show that S (x, y) is definable in existential Büchi arithmetic. Since y = p ·i · x if and only if y ≡ x mod (p − 1), one can obtain S as

We slightly generalize S . Let U ⊆ N, define the predicate S U (x, y) to hold whenever x = p r and y = p r+u for some r ≥ 0 and u ∈ U .

Lemma 6. For any ultimately periodic set U ⊆ N, the predicate S U (x, y) is definable in existential Büchi arithmetic

Proof. Suppose that U is given as (t, , B, R), we define

Towards proving Theorem 3, we now show that we can define w * p for any w ∈ Σ p . Lemma 7. For any w ∈ Σ * p , w * p is definable by a formula of existential Büchi arithmetic Φ w * (x).

Proof. Let m = p be the smallest power of p greater than w p . Then for any k > 0,

It follows that w * p is defined by

Building upon Lemma 7, we now show that, for any w ∈ Σ p , we can define w + p shifted to the left by a number of zeros specified by an ultimately periodic set.

Lemma 8. Let w ∈ Σ * p and U be an ultimately periodic set. Then w + 0 U p is definable by a formula of existential Büchi arithmetic Φ U,w + (x).

Proof. The case w ∈ 0 * is trivial. Thus, let w = w · w 0 such that w ∈ Σ * p · (Σ p \ {0}) and w 0 ∈ 0 * . Observe that for i < j, w j p − w i p = w j−i 0 i p . We define

The first line defines the set w + 0 * p , whereas the second line ensures that the tailing number of zeros is in the set U + |w 0 |.

We have now all the ingredients to prove the following key proposition.

Then L p is definable in existential Büchi arithmetic.

Proof. The proposition follows from showing the statement for languages of the form

We show the statement by induction on k. The induction base case k = 0 is trivial. For the induction step, assume that for M = v 1 w + 2 v 2 · · · v k−1 w + k v k , M p is defined by a formula Φ k (x) of existential Büchi arithmetic, and let v 0 , w 1 ∈ Σ * p . We first show how to define N = w

Observe that M p = Φ k (x) p , and that both U = {|w| : w ∈ M } and V = {|w| : w ∈ M 0 } are ultimately periodic sets, cf. [6, 12] . We moreover assume that w 1 ∈ 0 * , otherwise we are done. Factor w 1 = w · w 0 such that w ∈ Σ * p · (Σ p \ {0}) and w 0 ∈ 0 * .

Recall that W p (x, y) holds if and only if y is the smallest power of p strictly greater than x, and define Ψ k+1 (x) := ∃y ∃z : Φ k (y) ∧ Φ U,w + (z) ∧ x = y + z∧ ∧ ∃s ∃t : W p (y, s) ∧ S V (s, t) ∧ V p (p |w0|+1 · t, z) .

The first line composes x as the sum of some y ∈ M p and z ∈ w + 0 U p . The second line ensures that the number of zeros between the leading bit of y and the last non-zero digit of z in their p-ary expansion is in V + |w 0 |. Thus,

We now show how to define L along similar lines. To this end, factor N = N 0 · N such that N 0 ⊆ 0 * and N ⊆ (Σ p \ {0}) · Σ * p , and let T = {|w| : w ∈ N 0 }, which is an ultimately periodic set. We now obtain the desired formula of existential Büchi arithmetic as

Since we can define any regular language of the form (2) in existential Büchi arithmetic via Proposition 2, we can define a finite union of such languages and thus define all regular languages of polynomial growth in existential Büchi arithmetic. This completes the proof of Theorem 3.

Note that PREG p ⊆ PA for any base p ≥ 2: since M = Φ(x) is ultimately periodic for any formula Φ(x) of Presburger arithmetic, whenever Φ(x) is infinite it follows that d M (n) = Ω(p n ), i.e., not of polynomial growth.

The main result of this paper is that existential Büchi arithmetic is strictly less expressive than full Büchi arithmetic of any base. This is in contrast to Presburger arithmetic, for which it is known that its existential fragment is expressively complete.

When considered as the first-order theory of the structure N, 0, 1, + , Presburger arithmetic does not have a quantifier elimination procedure. The extended structure N, 0, 1, +, {c|·} c>1 , however, admits quantifier elimination. Those additional divisibility predicates are definable in existential Presburger arithmetic. Our main result shows that even if we extended the structure underlying Büchi arithmetic with predicates definable in existential Büchi arithmetic, the resulting first-order theory would not admit quantifier-elimination. On the positive side, Benedikt et al. [1, Thm. 3.1] give an extension of Büchi arithmetic which has quantifier elimination.

We conclude this paper with an interesting yet likely challenging open problem: Is it decidable whether a set definable in Büchi arithmetic is definable in existential Büchi arithmetic? The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Definable relations and first-order query languages over strings

Entiers et automates finis. Mémoire de fin d'études

Logic and p-recognizable sets of integers

Weak second-order arithmetic and finite automata

The taming of the semi-linear set

Finite automata and unary languages

Bounded ALGOL-like languages

On the existential theories of Büchi arithmetic and linear p-adic fields

Knapsack and the power word problem in solvable Baumslag-Solitar groups

Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt

Characterizing regular languages with polynomial densities

Unary finite automata vs. arithmetic progressions

The theory of

On the construction of automata from linear arithmetic constraints

Acknowledgments. We would like to thank Dmitry Chistikov and Alex Fung for inspiring discussions on the topics of this paper, and the FoSSaCS'21 reviewers for their comments and suggestions.This work is part of a project that has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT).