In the early 1960s, R. J. Büchi made a fundamental discovery: decidability of arithmetic theories can be established using automata theory. Moreover, the exact expressive power of finite automata can be described via an extension of Presburger arithmetic, which is now known as Büchi arithmetic. The nature of this theory is radically different from the well-studied Presburger arithmetic, and for this reason the classical questions of complexity and expressivity for Büchi arithmetic remained unsolved for a long time.
In my talk, I will first give a sketch of the proof of the Büchi's theorem and then show the relationships between Büchi arithmetic and the integer arithmetic of addition and usual bitwise operations NOT, AND, OR. Next, I will show why the quantifier-elimination approach, which is not applicable to prove decidability of Büchi arithmetic, becomes a powerful tool for studying the expressive power of its existential fragment. Finally, it will be shown that the developed quantifier-elimination techniques can be combined with the decision procedure for Presburger arithmetic with the base 2 exponentiation. This combination provides a new algorithm for the integer linear-exponential programming feasibility, which was (before 2024) only known to be decidable in exponential space using a purely automata-theoretic procedure. In contrast, the quantifier-elimination procedure runs in non-deterministic polynomial time.