2
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

I don't see any gap in your understanding. What you wrote looks correct to me.

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.

Good job catching this!

$\endgroup$
  • $\begingroup$ I'm marking this as the answer. I emailed the author hoping he could clarify his intentions but, alas, he did not reply. This is a shame since this example is used a lot on the rest of his slide decks. For me, the answer is: P as is not strong enough to be k-inductive, but if we strengthen it a bit, it becomes inductive. $\endgroup$ – MuchToLearn Nov 15 '19 at 23:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.