I'm following the slides at https://homepage.cs.uiowa.edu/~tinelli/talks/FT-11.pdf where Tinelli explains how k-induction works in the context of SMT based model checking.
A parametric and resettable counter is given as a Kripke structure by the following formulas:
Variables:
- $x := (c, n, r, n_0)$, where:
- $n_0$ is a positive integer (input)
- $r$ is a boolean (input)
- $c$, $n$ are integers (internal variables)
Initialization:
- $I[x] := (c = 1) \wedge (n = n_0)$
Transitions:
- $\begin{align*} T[x,x'] := (n' = n) & \wedge (& (r' \vee (c=n)) & \to (c' = 1)) \\ & \wedge (& \neg(r' \vee (c=n)) & \to (c' = c + 1)) \\ \end{align*}$
Property to prove invariant:
- $P[x] := c \le n + 1$
Tinelli uses the following notation:
$I^i:=I[x^{(i)}],P^i:=P[x^{(i)}],T^i:=T[x^{(i−1)},x^{(i)}]$.
He then claims on page 52/90 that the formula $P := c \le n+1$ is an invariant of this system because $P$ is 1-inductive (while incidentally not being 0-inductive). If I'm following correctly, this means that $I^0 \models P^0$ and $I^0 \wedge T^1 \models P^1$ (base case) and $P^0 \wedge P^1 \wedge T^1 \wedge T^2 \models P^2$ (inductive step). In particular it means that the formula $P^0 \wedge P^1 \wedge T^1 \wedge T^2 \wedge \neg (P^2)$ is UNSAT. However, after playing a little with Z3Py I was able to find the following model for this formula and a corresponding representation of a state transition trace with $(c,n,r)$:
- $c^0 = -1, n^0 = 0, c^1 = 1, n^1 = 0, r^1 = \text{True},c^2 = 2, n^2 = 0, r^2 = \text{False}$
- $(-1, 0, *) \to (1, 0, \text{True}) \to (2, 0, \text{False})$
Intuitively this makes sense. The constraint on $n_0$ being a positive integer affects the base case formula $I^0$ but not the inductive step, and therefore the above model is a valid model of the induction formula for $i=1$ which means the implication fails.
Of course $P$ is an invariant of this system, but it would seem to me that we cannot show it with k-induction for k = 1.
What is the gap in my understanding of this material?
