Post History

As far as I'm aware, quantifier elimination in Presburger arithmetic and the translation to finite state automata are unrelated.

Given a formula $\varphi(x)$ in Presburger arithmetic, we can translate it to an automaton / regular expression $A$ on the characters $0$ and $1$ that reads in $x$ in binary and accepts iff $\varphi$ is true of $x$.

In order to get more variables involved, so, for instance, we can deal with formulas with more quantifiers, we need a way of feeding in multiple words, in this case multiple numbers in binary, into an automaton.

If we tried to feed them in sequentially, we'd want something like an automaton that can read in words on the alphabet $\{0,1,+,=\}$ like "101+11=1000" and tell us if they're true. The problem is that by the time we hit the plus sign, the automaton needs to have the entire first summand in memory, and we can't fit arbitrarily large summands in finite memory.

So what we'll do is we'll pad our numbers to be the same length and feed them in simultaneously. For instance, the sum above becomes

$$\begin{pmatrix}0\\0\\1\end{pmatrix}\begin{pmatrix}1\\0\\0\end{pmatrix}\begin{pmatrix}0\\1\\0\end{pmatrix}\begin{pmatrix}1\\1\\0\end{pmatrix}$$

The first row is our first addend, the second row is our second addend, and the third row is our sum. We feed this into our automaton as a word of $3$-vectors on $\{0,1\}$. (There are only $8$ of them, so it's still a finite alphabet.)

You can create an automaton / regular expression that accepts only correct addition facts when entered in this way. It's a little bit easier to construct this automaton if you decide to read in the input from right to left, but ultimately it doesn't matter which convention you decide on. 

This automaton corresponds to the formula $\varphi(x,y,z) \equiv x+y=z$ in Presburger arithmetic.

So the translation is: given a formula $\varphi$ in Presubrger arithmetic with free variables $x_1,\ldots,x_n$, there is an automaton / regular language on the alphabet $\{0,1\}^n$ that accepts a tuple of numbers read in simultaneously iff $\varphi$ holds of that tuple of numbers.

And the translation is almost exact: given an automaton that reads in a tuple of numbers fed in in binary simultaneously, there's a formula in Büchi arithmetic (<https://en.wikipedia.org/wiki/B%C3%BCchi_arithmetic>) that's equivalent to it. Büchi arithmetic is Presburger arithmetic with an added function $V_2(x)$ which returns the largest power of $2$ dividing $x$. If you want to read more, you're likely to find more information looking into why Büchi arithmetic is equivalent to finite automata.

You might be able to use this to get quantifier elimination in Presburger arithmetic, but the technique I know of is explained in Christoph Haase's "A Survival Guide to Presburger Arithmetic" https://www.cs.ox.ac.uk/people/christoph.haase/home/publication/haa-18/haa-18.pdf which essentially boils down to this:

To get quantifier elimination in Presburger arithmetic, you need to add inequalities and the ability to assert that two terms are equivalent modulo various natural numbers.

Any formula in this augmented Presburger arithmetic of the form $\exists y: \varphi(x_1,\ldots,x_n,y)$ asserts a bunch of inequalities and modular congruences for $ky$ for some constant $k$. Replace $ky$ with $z$, so we're asserting an extra modular congruence that $z$ is congruent to $0$ mod $k$.

By the Chinese remainder theorem, we're just searching for a $z$ with particular congruences modulo some big modulus $M$. To do this, we only need to search the $M$ entries on the left or right ends of the ranges given by the inequalities.

For instance, if we want to eliminate the quantifier from 
$$\exists z: (3a+4b \leq z \leq 5a+2b+10) \wedge (z \equiv 12a+2b+7 (\text{mod} 5)),$$ we just need to check to see if one of: $3a+4b, 3a+4b+1, 3a+4b+2, 3a+4b+3,$ or $3a+4b+4$ works for $z$. i.e. we can convert this $\exists z: \varphi(yza,b)$ to $$\varphi(3a+4b,a,b) \vee \cdots \vee \varphi(3a+4b+4,a,b).$$