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 ?
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&lt;\bar v,Init,Next, Bad\right&gt;$ 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&lt;term\right&gt;$,
$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 = &lt;term&gt;)
   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&lt;term\right&gt;$. $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&lt;term\right&gt;$.


Thus $\phi$ is an inductive invariant separator for $\left&lt;\bar v,Init,Next, Bad\right&gt;$ 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.