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.
