# Decidability of inductive invariant existence in Presburger arithmetic

Problem:

Consider a finite number of control states (including an "initial" and a "bad" state), a finite number of integer variables, and for each ordered pair of states a transition relation expressed in Presburger arithmetic.

Decide whether there exists an inductive invariant (= stable by post-states of the transition relation) containing the initial but not the bad state, definable in Presburger arithmetic.

(Note that this problem is different from the reachability problem in Presburger arithmetic, which is clearly undecidable (by reduction from two-counter machines).)

I suspect this problem is undecidable, but do not know of any proof for it. (It is obviously semidecidable.) Has somebody proved this ?

• I think we need to clarify this a tiny bit: the states are represented by an integer $n, m$, and the transition relation is a formula $\phi(n,m)$, with a formula $\psi_{\mathrm{good}}(n)$ and $\psi_{\mathrm{bad}}(n)$ that represent the initial states and bad states respectively? And you are looking for a formula $I(n)$ such that: $I(n)\wedge\phi(n,m) \rightarrow I(m)$, $\psi_{\mathrm{good}}(n) \rightarrow I(n)$ and $\psi_{\mathrm{bad}}(n) \rightarrow \neg I(n)$. Is this correct? – cody Apr 7 '14 at 21:49
• Yes, except that $n$ and $m$ are not single integers, but finite vectors of integers of fixed dimension $d$ ("finite number of integer variables"). Thanks for the clarification. – David Monniaux Apr 8 '14 at 7:24
• So what is the reachability problem? If it's just "the state $\psi_{\mathrm{bad}}(k)$ is reachable", then it's easy to show that the problems are equivalent: if $\psi_{\mathrm{bad}}(k)$ is unreachable, take $I(k)$ to be $\psi_{\mathrm{good}}(k)\vee(\forall y, \phi(y,k)\wedge\neg\psi_{\mathrm{bad}}(y)\rightarrow \neg\psi_{\mathrm{bad}}(k))$. Am I missing something? – cody Apr 8 '14 at 17:54
• Sorry, 1) it's $I(n) \rightarrow \psi_{\textrm{bad}}(n)$ 2) why should your set be inductive? for instance, why should $\psi_{\textrm{good}}(k) \land \phi(k,k') \rightarrow I(k')$? – David Monniaux Apr 9 '14 at 18:52

The inductive invariant separator problem for Presburger arithmetic is undecidable.

I am unaware of a proof in the literature to point you at. (It seems so straightforward a question I assume it is somewhere out there.) The proof I came up with follows roughly the same construction as the halting problem. Here is a brief overview. We first assume a decision procedure $D$ exists and then construct a machine $S$ with input $M$. $S$ uses $D$ to decide non-termination of $M$ on itself and then $S$ reverses the output. We then use the construction of $S$ to show that $D$ must give an incorrect answer on the execution of $S$ on itself.

Instead of a reduction to the halting problem, the proof is for all intents and purposes a restatement of the proof of the halting problem. It is a bit verbose as will require that the exact strongest post condition can be expressed. (If a simpler proof is possible, I'd be very interested in hearing it.) Now on to the gory details.

The inductive invariant separator problem for Presburger arithmetic is for a given 4-tuple $\left<\bar v,Init,Next, Bad\right>$ where $\bar v$ is a finite set of variable names, $Init$ and $Bad$ are Presburger formulas whose free variables are in $\bar v$, $Next$ is Presburger formula whose free variables are in $\bar v$ or $\bar{v}'$ (a primed copy of $\bar v$) does there exist a formula $\phi$ in Presburger arithmetic with free variables in $\bar v$ such that:

• $Init \implies \phi$
• $\phi \land Next \implies \phi'$
• $\phi \implies \lnot Bad$

where $\phi'$ primes all of the free variables in $\phi$.

Suppose this problem is decidable. There then exists a Turing machine $D'$ that decides the separator problem (for a given encoding of Presburger formulas). Let $D$ be a deterministic Turing Machine that simulates $D'$. $D$ terminates and decides the separator problem.

A variable assignment over a finite set of variables $\{v_i\}$ is a conjunction $\bigwedge v_i = c_i$ where $c_i$ is an integer constant.

I will also assume the existence of a Turing machine to Presburger arithmetic compiler $C$ with some reasonable, but strong restrictions. $C$ takes as input a Turing machine $M$ with a unique final state, $term$, and an input $w$, and constructs presburger formulas $Init$ and $Next$ over a finite set of variables $\bar v$. Informally we require the paths of the Presburger formulas to simulate the execution of $M$ on $w$. Further, we require it to be a step simulation. Formally, we require that:

• $C$ assigns a unique constant to all control states in $M$ and let the constant for $term$ be $\left<term\right>$,
• $C$ includes a variable $pc$ in $\bar v$ that tracks the control state of $M$ at every step in the execution,
• $C$ generates $Init$ to be in the form of a variable assignment over $\bar v$,
• $C$ ensures that $Next$ to have a unique successor on variable assignments over $\bar v$ (that are reachable from $Init$) if $M$ is deterministic,
• for there to exist an injective function $f$ from a state of $M$ (control and tape) to a variable assignment over $bar v$ such that $Next$ has a successor, the initial state of $M$ on $w$ is mapped to exactly $Init$ and the control state of $M$ consistently assigns $pc$,
• $C$ is deterministic, and
• $C$ terminates.

Now construct the Turing machine $S$ that takes a Turing machine $M$ as input and does the following (in pseudocode):

S(M):
Run C(M,M) to get v, Init and Next
Simulate D on v, Init, Next, Bad := (pc = <term>)
If D says a separator exists:
terminate
If D says no separator exists:
loop: goto loop

We now show $D$ cannot give a consistent answer on $S$ with the input $S$. Start executing $S(S)$. $C$ terminates with $Init$ and $Next$ that can simulate $S$ with the input $S$. We now setup a correspondence between state $i$ of the execution of $S(S)$, $s_i$, and the $i$th variable assignment $\bar v_i = f(s_i)$ of the execution of $Next$ starting from $Init$. $S$ is deterministic by construction so by the properties of $C$, $Next$ must have unique successors on variable assignments and $Init$ is a variable assignment. (For reference, $f(s_0)=\bar v_i=Init$.)

Suppose $D$ says a separator exists. Let $\phi$ be such a separator. The execution of $S(S)$ then reaches $term$ in $k$ steps. (This includes executing $C$ and $D$.) Now $\bar v_1 \ldots \bar v_k$ is a counter example to $\phi$ being a separator as it reaches $pc = \left<term\right>$. $D$ gave an inconsistent answer.

Now suppose $D$ says no such separator exists. $S(S)$ then reaches the control state $loop$ in $k$ steps. All states after $k$ are then identical $s_{k+1}=s_{k+2}=\ldots$. The corresponding variables assignment sequence after $k$ must then assign each variable to the same constant. Let $\phi = \bigvee_{i=1}^{k+1} \bar v_i$. (Note: $\phi$ is now exactly the reachable variable assignments by $Next$ starting from $Init$.) Then

• $Init \implies \phi$ as $Init$ is exactly $\bar v_1$.
• $\phi \land Next \implies \phi'$ as $Next$ is deterministic and for all $i$ if $\bar v_i$ holds then $\bar v_{i+1}'$ holds.
• $\phi \implies \lnot Bad$ as each variable assignment $\bar v_i$ implies $pc \neq \left<term\right>$.

Thus $\phi$ is an inductive invariant separator for $\left<\bar v,Init,Next, Bad\right>$ and $D$ gave an inconsistent answer.

$D$ must always give an inconsistent answer and thus a decision procedure does not exist.

Doing this exercise really made me appreciate Jerome Leroux's work on separators for vector addition systems.

• This is great, thanks! Do you have a reference for step 2, namely the "compiler from TM to Presburger Arithmetic"? That seems to be the crux of the proof. – cody Apr 16 '14 at 19:35
• We can use the standard Turing machine reduction to Minsky machines to the naive Presburger encoding. Then every Turing machine state $i$ eventually has a matching Presburger state $i'$ (with $i \leq i'$). The model I had in mind roughly assumes the tape is in binary and there 1 variable for the tape $t$, a variable that is maintained to be the position $2^p$ if the head of M is at position $p$ and uses $2^p$ to split $t$ into 3 variables $\exists l,c,r$ where $l \leq 2^p, c < 2, r \geq 2^{p+1}$ and $(l + p + r = t => c=1)$ or $(l + r = t => c=0)$. Hope the rest of the encoding is clear. – Tim Apr 16 '14 at 22:41