# Proving that a property is k-inductive with an SMT solver (parametric resettable counter)

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?

Perhaps the author meant to use the property $$P := c \le n+1 \land n \ge 1$$. I think with that modification, $$P$$ becomes 1-inductive but not 0-inductive. I suspect the author was looking for a simple example of a property that is 1-inductive but not 0-inductive, and missed a small detail.