LTL model checking

Suppose that, given a system module M specifying a rewrite theory $\mathcal{R} = (\Sigma,E,\phi,R)$, we have:

• chosen a kind $k$ in M as our kind of states;
• defined some state predicates $\Pi$ and their semantics in a module, say M-PREDS, protecting M by the method already explained in Section 10.2.

Then, as explained in Section 10.2, this defines a Kripke structure $\mathcal{K}({\cal R},k)_{\Pi}$ on the set of atomic propositions $AP_{\Pi}$. Given an initial state $[t] \in T_{\Sigma/E,k}$ and an LTL formula $\varphi \in LTL(AP_{\Pi})$ we would like to have a procedure to decide the satisfaction relation

$$\mathcal{K}({\cal R},k)_{\Pi},[t] \models \varphi.$$

In general this relation is undecidable. It becomes decidable if two conditions hold:

1. the set of states in $T_{\Sigma/E,k}$ that are reachable from $[t]$ by rewriting is finite,^10.1 and
2. the rewrite theory $\mathcal{R} = (\Sigma,E,\phi,R)$ specified by M plus the equations $D$ defining the predicates $\Pi$ are such that:
   • both $E$ and $E \cup D$ are (ground) Church-Rosser and terminating, perhaps modulo some axioms $A$, with $(\Sigma, E) \subseteq (\Sigma \cup \Pi, E \cup D)$ a protecting extension, and
   • $R$ is (ground) coherent relative to $E$ (again, perhaps modulo some axioms $A$).

Under these assumptions, both the state predicates $\Pi$ and the transition relation $\rightarrow^{1}_{{\cal R}}$ are computable and, given the finite reachability assumption, we can then settle the above satisfaction problem using a model-checking procedure.

Specifically, Maude uses an on-the-fly LTL model-checking procedure of the style described in [11]. The basis of this procedure is the following. Each LTL formula $\varphi$ has an associated Büchi automaton $B_{\varphi}$ whose acceptance $\omega$-language is exactly that of the behaviors satisfying $\varphi$. We can then reduce the satisfaction problem

$$\mathcal{K}({\cal R},k)_{\Pi},[t] \models \varphi$$

to the emptiness problem of the language accepted by the synchronous product of $B_{\neg \varphi}$ and (the Büchi automaton associated with) $(\mathcal{K}({\cal R},k)_{\Pi},[t])$. The formula $\varphi$ is satisfied if and only if such a language is empty. The model-checking procedure checks emptiness by looking for a counterexample, that is, an infinite computation belonging to the language recognized by the synchronous product. For a detailed explanation of this general method of on-the-fly LTL model checking, see [11]; and for a discussion of the specific techniques used in the Maude LTL model-checker implementation, see [39].

This makes clear our interest in obtaining the negative normal form of a formula $\neg \varphi$, since we need it to build the Büchi automaton $B_{\neg \varphi}$. For efficiency purposes we need to make $B_{\neg \varphi}$ as small as possible. The following module LTL-SIMPLIFIER (also in the model-checker.maude file) tries to further simplify the negative normal form of the formula $\neg \varphi$ in the hope of generating a smaller Büchi automaton $B_{\neg \varphi}$. This module is optional (the user may choose to include it or not when doing model checking) but tends to help building a smaller $B_{\neg \varphi}$.

  fmod LTL-SIMPLIFIER is
    including LTL .

    *** The simplifier is based on:
    ***   Kousha Etessami and Gerard J. Holzman,
    ***   "Optimizing Buchi Automata", CONCUR 2000, LNCS 1877.
    *** We use the Maude sort system to do much of the work.

    sorts TrueFormula FalseFormula PureFormula PE-Formula PU-Formula .
    subsort TrueFormula FalseFormula < PureFormula <
            PE-Formula PU-Formula < Formula .

    op True : -> TrueFormula [ctor ditto] .
    op False : -> FalseFormula [ctor ditto] .
    op _/\_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] .
    op _/\_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] .
    op _/\_ : PureFormula PureFormula -> PureFormula [ctor ditto] .
    op _\/_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] .
    op _\/_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] .
    op _\/_ : PureFormula PureFormula -> PureFormula [ctor ditto] .
    op O_ : PE-Formula -> PE-Formula [ctor ditto] .
    op O_ : PU-Formula -> PU-Formula [ctor ditto] .
    op O_ : PureFormula -> PureFormula [ctor ditto] .
    op _U_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] .
    op _U_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] .
    op _U_ : PureFormula PureFormula -> PureFormula [ctor ditto] .
    op _U_ : TrueFormula Formula -> PE-Formula [ctor ditto] .
    op _U_ : TrueFormula PU-Formula -> PureFormula [ctor ditto] .
    op _R_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] .
    op _R_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] .
    op _R_ : PureFormula PureFormula -> PureFormula [ctor ditto] .
    op _R_ : FalseFormula Formula -> PU-Formula [ctor ditto] .
    op _R_ : FalseFormula PE-Formula -> PureFormula [ctor ditto] .

    vars p q r s : Formula .
    var pe : PE-Formula .
    var pu : PU-Formula .
    var pr : PureFormula .

    *** Rules 1, 2 and 3; each with its dual.
    eq (p U r) /\ (q U r) = (p /\ q) U r .
    eq (p R r) \/ (q R r) = (p \/ q) R r .
    eq (p U q) \/ (p U r) = p U (q \/ r) .
    eq (p R q) /\ (p R r) = p R (q /\ r) .
    eq True U (p U q) = True U q .
    eq False R (p R q) = False R q .

    *** Rules 4 and 5 do most of the work.
    eq p U pe = pe .
    eq p R pu = pu .

    *** An extra rule in the same style.
    eq O pr = pr .

    *** We also use the rules from:
    ***   Fabio Somenzi and Roderick Bloem,
    ***   "Efficient Buchi Automata from LTL Formulae",
    ***   p247-263, CAV 2000, LNCS 1633.
    *** that are not subsumed by the previous system.

    *** Four pairs of duals.
    eq O p /\ O q = O (p /\ q) .
    eq O p \/ O q = O (p \/ q) .
    eq O p U O q = O (p U q) .
    eq O p R O q = O (p R q) .
    eq True U O p = O (True U p) .
    eq False R O p = O (False R p) .
    eq (False R (True U p)) \/ (False R (True U q))
      = False R (True U (p \/ q)) .
    eq (True U (False R p)) /\ (True U (False R q))
      = True U (False R (p /\ q)) .

    *** <= relation on formula
    op _<=_ : Formula Formula -> Bool [prec 75] .

    eq p <= p = true .
    eq False <= p  = true .
    eq p <= True = true .

    ceq p <= (q /\ r) = true if (p <= q) /\ (p <= r) .
    ceq p <= (q \/ r) = true if p <= q .
    ceq (p /\ q) <= r = true if p <= r .
    ceq (p \/ q) <= r = true if (p <= r) /\ (q <= r) .

    ceq p <= (q U r) = true if p <= r .
    ceq (p R q) <= r = true if q <= r .
    ceq (p U q) <= r = true if (p <= r) /\ (q <= r) .
    ceq p <= (q R r) = true if (p <= q) /\ (p <= r) .
    ceq (p U q) <= (r U s) = true if (p <= r) /\ (q <= s) .
    ceq (p R q) <= (r R s) = true if (p <= r) /\ (q <= s) .

    *** conditional rules depending on <= relation
    ceq p /\ q = p if p <= q .
    ceq p \/ q = q if p <= q .
    ceq p /\ q = False if p <= ~ q .
    ceq p \/ q = True if ~ p <= q .
    ceq p U q = q if p <= q .
    ceq p R q = q if q <= p .
    ceq p U q = True U q if p =/= True /\ ~ q <= p .
    ceq p R q = False R q if p =/= False /\ q <= ~ p .
    ceq p U (q U r) = q U r if p <= q .
    ceq p R (q R r) = q R r if q <= p .
  endfm

Suppose that all the requirements listed above to perform model checking are satisfied. How do we then model check a given LTL formula in Maude for a given initial state $[t]$ in a module M? We define a new module, say M-CHECK, according to the following pattern:

  mod M-CHECK is
    protecting M-PREDS .
    including MODEL-CHECKER .
    including LTL-SIMPLIFIER . *** optional
    op init : -> k .           *** optional
    eq init = t .              *** optional
  endm

The declaration of a constant init of the kind of states is not necessary: it is a matter of convenience, since the initial state t may be a large term.

The module MODEL-CHECKER (in the file model-checker.maude) is as follows:

  fmod MODEL-CHECKER is
    protecting QID .
    including SATISFACTION .
    including LTL .
    subsort Prop < Formula .
   
    *** transitions and results
    sorts RuleName Transition TransitionList ModelCheckResult .
    subsort Qid < RuleName .
    subsort Transition < TransitionList .
    subsort Bool < ModelCheckResult .
    ops unlabeled deadlock : -> RuleName .
    op {_,_} : State RuleName -> Transition [ctor] .
    op nil : -> TransitionList [ctor] .
    op __ : TransitionList TransitionList -> TransitionList
         [ctor assoc id: nil] .
    op counterexample :
         TransitionList TransitionList -> ModelCheckResult [ctor] .

    op modelCheck : State Formula ~> ModelCheckResult
         [special (...)] .
  endfm

Its key operator is modelCheck (whose special attribute has been omitted here), which takes a state and an LTL formula and returns either the Boolean true if the formula is satisfied, or a counterexample when it is not satisfied. Note that the sort Prop coming from the SATISFACTION module is declared as a subsort of Formula in LTL. In each concrete use of MODEL-CHECKER, such as that in M-CHECK above, the atomic propositions in Prop will have been specified in a module such as M-PREDS.

Let us illustrate the use of this operator with our MUTEX example. Following the pattern described above, we can define the module

  mod MUTEX-CHECK is
    protecting MUTEX-PREDS .
    including MODEL-CHECKER .
    including LTL-SIMPLIFIER .
    ops initial1 initial2 : -> Conf .
    eq initial1 = $ [a, wait] [b, wait] .
    eq initial2 = * [a, wait] [b, wait] .
  endm

The relationships between all the modules involved at this point is illustrated in Figure 10.1, where a single arrow represents an including importation and a triple arrow represents a protecting importation.

Figure 10.1: Importation graph of model-checking modules

We are then ready to model check different LTL properties of MUTEX. The first obvious property to check is mutual exclusion:

  Maude> red modelCheck(initial1, [] ~(crit(a) /\ crit(b))) .
  reduce in MUTEX-CHECK :
    modelCheck(initial1, []~ (crit(a) /\ crit(b))) .
  result Bool: true

  Maude> red modelCheck(initial2, [] ~(crit(a) /\ crit(b))) .
  reduce in MUTEX-CHECK :
    modelCheck(initial2, []~ (crit(a) /\ crit(b))) .
  result Bool: true

We can also model check the strong liveness property that if a process waits infinitely often, then it is in its critical section infinitely often:

  Maude> red modelCheck(initial1, ([]<> wait(a)) -> ([]<> crit(a))) .
  reduce in MUTEX-CHECK :
    modelCheck(initial1, []<> wait(a) -> []<> crit(a)) .
  result Bool: true

  Maude> red modelCheck(initial1, ([]<> wait(b)) -> ([]<> crit(b))) .
  reduce in MUTEX-CHECK :
    modelCheck(initial1, []<> wait(b) -> []<> crit(b)) .
  result Bool: true

  Maude> red modelCheck(initial2, ([]<> wait(a)) -> ([]<> crit(a))) .
  reduce in MUTEX-CHECK :
    modelCheck(initial2, []<> wait(a) -> []<> crit(a)) .
  result Bool: true

  Maude> red modelCheck(initial2, ([]<> wait(b)) -> ([]<> crit(b))) .
  reduce in MUTEX-CHECK :
    modelCheck(initial2, []<> wait(b) -> []<> crit(b)) .
  result Bool: true

Of course, not all properties are true. Therefore, instead of a success we can get a counterexample showing why a property fails. Suppose that we want to check whether, beginning in the state initial1, process b will always be waiting. We then get the counterexample:

  Maude> red modelCheck(initial1, [] wait(b)) .
  reduce in MUTEX-CHECK : modelCheck(initial1, []wait(b)) .
  result ModelCheckResult:
    counterexample({$ [a, wait] [b, wait], 'a-enter}
                   {[a, critical] [b, wait], 'a-exit}
                   {* [a, wait] [b, wait], 'b-enter},
                   {[a, wait] [b, critical], 'b-exit}
                   {$ [a, wait] [b, wait], 'a-enter}
                   {[a, critical] [b, wait], 'a-exit}
                   {* [a, wait] [b, wait], 'b-enter})

The main constructors used in the syntax of a counterexample term are:

    op {_,_} : State RuleName -> Transition .
    op nil : -> TransitionList [ctor] .
    op __ : TransitionList TransitionList -> TransitionList
         [ctor assoc id: nil] .
    op counterexample :
         TransitionList TransitionList -> ModelCheckResult [ctor] .

Therefore, a counterexample is a pair consisting of two lists of transitions, where the first corresponds to a finite path beginning in the initial state, and the second describes a loop. This is because, if an LTL formula $\varphi$ is not satisfied by a finite Kripke structure, it is always possible to find a counterexample for $\varphi$ having the form of a path of transitions followed by a cycle [11]. Note that each transition is represented as a pair, consisting of a state and the label of the rule applied to reach the next state.

Let us finish this section with an example of how not to use the model checker. Consider the following specification:

  mod MODEL-CHECK-BAD-EX is
    including MODEL-CHECKER .
    extending LTL .
    sort Foo .
    op a : -> Foo .
    op f : Foo -> Foo .
    rl a => f(a) .

    subsort Foo < State .
    op p : -> Prop .
  endm

This module describes an infinite transition system of the form

$$\texttt{a} \rightarrow \texttt{f(a)} \rightarrow \texttt{f(f(a))} \rightarrow \texttt{f(f(f(a)))} \rightarrow \cdots,$$

where the property p is not satisfied anywhere. Therefore the state a does not satisfy, e.g., the property []p. However, if we try to invoke Maude with the command

  Maude> red in MODEL-CHECK-BAD-EX : modelCheck(a, []p) .

we run into a nonterminating computation.

Making explicit that p does not hold in a by adding the equation

  eq (a |= p) = false .

does not help. We run into the same problem even if the formula does not contain a temporal operator: modelCheck(a, p) does not terminate either. The reason is that the set of states reachable from a is not finite, and hence one of the main requirements for the model-checking algorithm is not satisfied.