LARA

Using automata to decide Presburger arithmetic

Minimalistic syntax for Presburger arithmetic is given by the following grammar:

F ::= V=1 | V=V | V=V+V | $\lnot$ F | F $\lor$ F | $\exists$ v. F

V ::= v_1 | v_2 | …

Variables range over non-negative integers.

Example formula: $x = y + 1 \land z = y + 1$

This is no loss of generality because we can express all other constructs using the given ones:

  • integers are equivalence classes of pairs of non-negative integers, replacing $(x^{+},x^{-}) = (y^{+},y^{-})$ with $x^{+} + y^{-} = y^{+} + x^{-}$, and expressing $(x^{+},x^{-})-(y^{+},y^{-})$ as $(x^{+},x^{-})+(y^{-},y^{+})$.
  • arbitrary additive constants: use binary notation and the addition operator and $x=1$ operator
  • multiplication by constant $c$: use addition, also binary development of $c$
  • $x \leq y$ is $\exists z. x + z = y$
  • $c$ divides $x$ is $\exists k. x = c \cdot k$
  • propositional operations: use $\lnot, \lor$
  • $\forall$: use $\lnot, \exists$

Automata for Presburger Arithmetic Formulas

Automaton for formula: $x = y + v \land z = y + v$ accepts certain strings in alphabet $\{x,y,z,v\} \to \{0,1\}$. An example string that this automaton accepts can be represented as follows: 

x:  0 0 1 0 0 
y:  1 1 0 0 0
z:  0 0 1 0 0
v:  1 0 0 0 0

This string represents the satisfying assignment $\{(x,4),\ (y,3),\ (z,4),\ (v,1)\}$ for the above formula. If we take the valid formula

\begin{equation*} \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) \end{equation*}

the corresponding automaton accepts all strings. (End of example.)

Consider a formula $F$ in this minimal syntax. Rename all bound variables to be mutually distinct and distinct from free variables. Let these variables be $v_1,\ldots,v_n$. For every subformulas $G$ of $F$ we construct an automaton $A(G)$ whose alphabet is $\{0,1\}^n$. This automaton will accept strings (elements of $(\{0,1\}^n)^*$ that encode $n$-tuples of integers for which $G$ is true. The automaton $A(G)$ simultaneously reads the bits of binary representations of all $n$ variables at once.

If $a_1, \ldots, a_k \in \{0,1\}$, let $N(a_1 \ldots a_k) = a_1 + 2 a_2 + \ldots + 2^{k-1} a_k$. That is, $N(w)$ denotes the value of the string $w$ viewed as a binary representation of a non-negative integer. We will define $A(G)$ such that for every $k$ and every matrix $a_{ij} \in \{0,1\}$, $1 \leq i \leq n$ and $1 \leq j \leq k$, the following correspondence holds:

\begin{equation*} e(G)(I)={\it true}, \mbox{ for } \alpha_I(v_j) = N(a_{j1} \ldots a_{jk}), \mbox{ for } 1 \le j \le n \end{equation*}

iff

\begin{equation*} (a_{11},a_{21},\ldots,a_{n1}) ... (a_{1k},a_{2k},\ldots,a_{nk}) \in L(A(G)) \end{equation*}

Graphically: 

a11 ... a1k         --->   v1
a21 ... a2k         --->   v2
... ... ...         ...
an1 ... ank         --->   vn

 ^
 |
L(G)

In matrix $a_{ij}$, row $i$ gives the value for variable $v_i$, whereas column $j$ gives the $j$-th symbol of the input word for the automaton.

Case $A(v_i=1)$

The automaton expects to see as the first symbol some $(a_1,\ldots,a_k)$ with $a_i=1$, if it finds it, it goes into accept state. If it ever encounters another symbol with $a_i=1$, then it goes into an error state.

Case $A(v_p=v_q)$

The automaton expects to see a sequence of symbols $(a_1,\ldots,a_k)$ with $a_p=a_q$ and transitions into an error state if a different symbol occurs.

Case $A(G_1 \lor G_2)$, $A(\lnot G)$

This follows from closure properties of finite state machines, take automata that denote union and complement of the languages.

Case $A(\exists v_i. G)$

(Sketch) This is projection operation on an automaton. Take $A(G)$ and replace each transition with label $(a_1,\ldots,a_i,\ldots,a_n)$ with two transitions $(a_1,\ldots,0,\ldots,a_n)$ and $(a_1,\ldots,1,\ldots,a_n)$ into the same destination state. The ideas is that existentially quantifying over an integer is similar to existentially quantifying over all of its bits. There are some subtleties that have to do with the length of the existentially quantified variables; we explain this when we give the more general construction for Weak Monadic Logic of One Successor.

Why the correspondence implies decidability. Consider a PA formula $F$. The following are equivalent:

  • $F$ is satisfiable
  • there exist some interpretation of free variables of $F$ such that $e(F)(I)={\it true}$
  • there exist some digits $a_{ij}$ such that $e(F)(I)={\it true}$ for $\alpha_I(v_j) = N(a_{j1} \ldots a_{jk})$
  • there exist some digits $a_{ij}$ such that $(a_{11},a_{12},\ldots,a_{1n}) ... (a_{k1},a_{k2},\ldots,a_{kn}) \in L(A(F))$
  • $L(A(F)) \neq \emptyset$
  • $A(F)$ has a reachable accepting state

Therefore, to check if $F$ is satisfiable, we construct $A(F)$ automaton and check whether the graph of $A(F)$ has a reachable accepting state.

Example: Step-by-step construction of automaton for

\begin{equation*} \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) \end{equation*}