Verifying infinite-state systems through abstractions

The bounded model checking of our two invariants for the readers and writers example up to depth $10^{6}$ greatly increases our confidence that the invariants hold, but, as already mentioned, bounded model checking is an incomplete procedure that falls short of being a proof: a counterexample at greater depth could exist.

Can we actually fully verify such invariants in an automatic way? One possible method is to verify the invariants through search not on the original infinite-state system, but on a finite-state abstraction of it, that is, on an appropriate quotient of the original system whose set of reachable states is finite. The paper [62] describes a simple method for, given a rewrite theory $\mathcal{R} = (\Sigma,E,\phi,R)$, defining an abstraction $\mathcal{A}$ of it: just add equations. That is, we can define our abstract theory as a rewrite theory $\mathcal{A} = (\Sigma,E\cup G,\phi,R)$, with $G$ a set of extra equations powerful enough to collapse the infinite set of reachable states into a finite set. This method can be used (with an additional deadlock-freedom requirement) to verify not just invariants, but in fact any LTL formula (see [62] and Section 13.4 of [16]).

Of course, the equations $G$ we add cannot be arbitrary. First of all, they should respect all the necessary executability assumptions, so that in $\mathcal{A} = (\Sigma,E\cup G,\phi,R)$ the equations $E \cup G$ should be ground Church-Rosser and terminating,^9.2 and the rules $R$ should be ground coherent with $E \cup G$. Furthermore, the equations $G$ should be invariant-preserving with respect to the invariants that we want to model check; that is, for any such invariant I and for any two ground terms $t,t'$ denoting states such that $t =_{E \cup G} t'$, it should be the case that $E \vdash \texttt{I}(t) = \texttt{I}(t')$.

A first key observation is that, if both $\mathcal{R}$ and $\mathcal{A}$ protect the sort Bool, that is, the only canonical forms of that sort are true and false, and $\texttt{true} \neq \texttt{false}$, then the equations $G$ are invariant-preserving. A second key observation is that we may be able to automatically check that a module protects the sort Bool by:

1. checking that it has no equations with true or false in the lefthand side;
2. checking that it is ground confluent and sort-decreasing with the Church-Rosser Checker (CRC) tool;
3. checking that it is terminating with the Maude Termination Tool (MTT); and
4. checking that it is sufficiently complete with the Sufficient Completeness Checker (SCC) tool.

Indeed, since true and false are the only constructors of sort Bool, (4) ensures the ``no junk'' part of protection, whereas (1)-(3) ensure the ``no confusion,'' $\texttt{true} \neq \texttt{false}$ part.

For invariant verification, the key property that an abstraction meeting these requirements satisfies is that, if I is one of the invariants preserved by $G$, then we have the implication

$$\mathcal{A}, \texttt{init} \models \Box \texttt{I} \;\;\; \L... ...rrow \;\;\; \mathcal{R}, \texttt{init} \models \Box \texttt{I}$$

Therefore, if we can verify the invariant on $\mathcal{A}$, we are sure that it also holds on $\mathcal{R}$. However, the fact that we find a counterexample in $\mathcal{A}$ does not necessarily mean that a counterexample exists for $\mathcal{R}$: it could be a spurious counterexample, caused by $\mathcal{A}$ being too coarse of an abstraction, and therefore having no counterpart in $\mathcal{R}$. In such cases, one possible approach is to refine our abstraction by imposing fewer equations.

We can illustrate these ideas by defining an abstraction of our readers-writers system. In order to check that the equations in our abstraction preserve the invariants, we need an explicit representation of those invariants. Since at present the CRC and MTT tools do not handle predefined modules like BOOL, we use instead a sort NewBool.

  mod READERS-WRITERS-PREDS is
    protecting READERS-WRITERS .
    sort NewBool .
    ops tt ff : -> NewBool [ctor] .
    ops mutex one-writer : Config -> NewBool [frozen] .
    eq mutex(< s(N:Nat), s(M:Nat) >) = ff .
    eq mutex(< 0, N:Nat >) = tt .
    eq mutex(< N:Nat, 0 >) = tt .
    eq one-writer(< N:Nat, s(s(M:Nat)) >) = ff .
    eq one-writer(< N:Nat, 0 >) = tt .
    eq one-writer(< N:Nat, s(0) >) = tt .
  endm

We can now define our abstraction, in which all the states having more than one reader and no writers are identified with the state having exactly one reader and no writer.

  mod READERS-WRITERS-ABS is
    including READERS-WRITERS-PREDS .
    including READERS-WRITERS .
    eq < s(s(N:Nat)), 0 > = < s(0), 0 > .
  endm

where the second including importation is needed because the READERS-WRITERS module is not protected, but would be assumed protected by default (because it is protected in READERS-WRITERS-PREDS) unless we explicitly declare it in including mode (see Section 6.1.3).

In order to check both the executability and the invariant-preservation properties of this abstraction, since we have no equations with either tt or ff in their lefthand side, we now just need to check:

1. that the equations in both READERS-WRITERS-PREDS and READERS-WRITERS-ABS are ground confluent, sort-decreasing, and terminating;
2. that the equations in both READERS-WRITERS-PREDS and READERS-WRITERS-ABS are sufficiently complete; and
3. that the rules in both READERS-WRITERS-PREDS and READERS-WRITERS-ABS are ground coherent with respect to their equations.

Regarding termination, since the equations of READERS-WRITERS-ABS contain those of the module READERS-WRITERS-PREDS, it is enough to check the termination of the equations in the former. The MTT tool, using the AProVE termination tool, checks this automatically.

Once the READERS-WRITERS-ABS and READERS-WRITERS-PREDS modules are available in Full Maude (see Section 14.1), we can check confluence of the equations by invoking the CRC as follows:

  Maude> (check Church-Rosser READERS-WRITERS-PREDS .)
  Church-Rosser checking of READERS-WRITERS-PREDS
  Checking solution:
    All critical pairs have been joined. The specification is
      locally-confluent.
  The specification is sort-decreasing.

  Maude> (check Church-Rosser READERS-WRITERS-ABS .)
  Church-Rosser checking of READERS-WRITERS-ABS
  Checking solution:
    All critical pairs have been joined. The specification is
      locally-confluent.
  The specification is sort-decreasing.

which finishes task (1).

Regarding (2), the SCC tool gives us:

  Maude> (scc READERS-WRITERS-PREDS .)
  Checking sufficient completeness of READERS-WRITERS-PREDS ...
  Success: READERS-WRITERS-PREDS is sufficiently complete under the 
    assumption that it is weakly-normalizing, confluent, and 
    sort-decreasing.

  Maude> (scc READERS-WRITERS-ABS .)
  Checking sufficient completeness of READERS-WRITERS-ABS ...
  Success: READERS-WRITERS-ABS is sufficiently complete under the 
    assumption that it is weakly-normalizing, confluent, and 
    sort-decreasing.

This leaves us with task (3), where the Coherence Checker (ChC) tool responds as follows:

  Maude> (check coherence READERS-WRITERS-PREDS .)
  Coherence checking of READERS-WRITERS-PREDS
  Coherence checking solution:
    All critical pairs have been rewritten and all equations
      are non-constructor.
    The specification is coherent.

  Maude> (check coherence READERS-WRITERS-ABS .)
  Coherence checking of READERS-WRITERS-ABS
  Coherence checking solution:
    The following critical pairs cannot be rewritten:
    cp < s(0), 0 > => < s(N*@:Nat), 0 > .

Of course, ground coherence means that all ground instances of this pair can be rewritten by a one-step rewrite up to canonical form by the equations. We can reason by cases and decompose this critical pair into two:

  cp < s(0), 0 > => < s(0), 0 > .
  cp < s(0), 0 > => < s(s(N:Nat)), 0 > .

Using the reduce command we can check that the canonical form of the term < s(s(N:Nat)), 0 > is < s(0), 0 >. Therefore, all we need to do is to check that < s(0), 0 > rewrites to itself (up to canonical form) in one step. We can do this check by giving the command:

  Maude> search in READERS-WRITERS-ABS : < s(0), 0 > =>1 X:Config .

  Solution 1 (state 0)
  states: 1  rewrites: 2 in 0ms cpu (26ms real) (~ rews/sec)
  X:Config --> < s(0), 0 >

  Solution 2 (state 1)
  states: 2  rewrites: 3 in 0ms cpu (124ms real) (~ rews/sec)
  X:Config --> < 0, 0 >

  No more solutions.

We have therefore completed all the checks (1)-(3) and can now automatically verify the two invariants on the abstract system, and therefore conclude that they hold in our original infinite-state readers-writers system, by executing the search commands:

  Maude> search in READERS-WRITERS-ABS : 
           < 0, 0 > =>* C:Config such that mutex(C:Config) = ff .

  No solution.
  states: 3  rewrites: 9 in 0ms cpu (0ms real) (~ rews/sec)

  Maude> search in READERS-WRITERS-ABS : 
           < 0, 0 > =>* C:Config such that one-writer(C:Config) = ff .

  No solution.
  states: 3  rewrites: 9 in 0ms cpu (0ms real) (~ rews/sec)