Chapter 10
LTL Model Checking

As pointed out in Section 1.4, given a Maude system module, we can distinguish two levels of specification:

This chapter discusses how a specific property specification logic, linear temporal logic (LTL), and a decision procedure for it, model checking, can be used to prove properties when the set of states reachable from an initial state in a system module is finite. It also explains how this is supported in Maude by its MODEL-CHECKER module, and other related modules, including the SAT-SOLVER module that can be used to check both satisfiability of an LTL formula and LTL tautologies. These modules are found in the file model-checker.maude.

Temporal logic allows specification of properties such as safety properties (ensuring that something bad never happens) and liveness properties (ensuring that something good eventually happens). These properties are related to the infinite behavior of a system. There are different temporal logics [21]; we focus on linear temporal logic [8621], because of its intuitive appeal, widespread use, and well-developed proof methods and decision procedures.

10.1 LTL formulas and the LTL module

Given a set AP of atomic propositions, we define the formulas of the propositional linear temporal logic LTL(AP) inductively as follows:

Other LTL connectives can be defined in terms of the above minimal set of connectives as follows:

The LTL syntax, in a typewriter approximation of the above mathematical syntax, is supported in Maude by the following LTL functional module (in the file model-checker.maude).

  fmod LTL is  
    protecting BOOL .  
    sorts Formula .  
    *** primitive LTL operators  
    ops True False : -> Formula [ctor format (g o)] .  
    op ~_ : Formula -> Formula [ctor prec 53 format (r o d)] .  
    op _/\_ : Formula Formula -> Formula  
         [comm ctor gather (E e) prec 55 format (d r o d)] .  
    op _\/_ : Formula Formula -> Formula  
         [comm ctor gather (E e) prec 59 format (d r o d)] .  
    op O_ : Formula -> Formula [ctor prec 53 format (r o d)] .  
    op _U_ : Formula Formula -> Formula  
         [ctor prec 63 format (d r o d)] .  
    op _R_ : Formula Formula -> Formula  
         [ctor prec 63 format (d r o d)] .  
    *** defined LTL operators  
    op _->_ : Formula Formula -> Formula  
         [gather (e E) prec 65 format (d r o d)] .  
    op _<->_ : Formula Formula -> Formula [prec 65 format (d r o d)] .  
    op <>_ : Formula -> Formula [prec 53 format (r o d)] .  
    op []_ : Formula -> Formula [prec 53 format (r d o d)] .  
    op _W_ : Formula Formula -> Formula [prec 63 format (d r o d)] .  
    op _|->_ : Formula Formula -> Formula [prec 63 format (d r o d)] .  
    op _=>_ : Formula Formula -> Formula  
         [gather (e E) prec 65 format (d r o d)] .  
    op _<=>_ : Formula Formula -> Formula [prec 65 format (d r o d)] .  
    vars f g : Formula .  
    eq f -> g = ~ f \/ g .  
    eq f <-> g = (f -> g) /\ (g -> f) .  
    eq <> f = True U f .  
    eq [] f = False R f .  
    eq f W g = (f U g) \/ [] f .  
    eq f |-> g = [](f -> (<> g)) .  
    eq f => g = [] (f -> g) .  
    eq f <=> g = [] (f <-> g) .  
  *** negative normal form  
    eq ~ True = False .  
    eq ~ False = True .  
    eq ~ ~ f = f .  
    eq ~ (f \/ g) = ~ f /\ ~ g .  
    eq ~ (f /\ g) = ~ f \/ ~ g .  
    eq ~ O f = O ~ f .  
    eq ~ (f U g) = (~ f) R (~ g) .  
    eq ~ (f R g) = (~ f) U (~ g) .  

Note that, for the moment, no set AP of atomic propositions has been specified in the LTL module. Section 10.2 explains how such atomic propositions are defined for a given system module M, and Section 10.3 explains how they are added to the LTL module as a subsort Prop of Formula in the MODEL-CHECKER module.

Note that the nonconstructor connectives have been defined in terms of more basic constructor connectives in the first set of equations. But since there are good reasons to put an LTL formula in negative normal form by pushing the negations next to the atomic propositions (this is specified by the second set of equations) we need to consider also the duals of the basic connectives , , U, and (respectively, True, O_, _U_, and _\/_) as constructors. That is, we need to also have as constructors the dual connectives: , R, and (respectively, False, _R_, and _/\_). Note that is self-dual.

10.2 Associating Kripke structures to rewrite theories

Since the models of temporal logic are Kripke structures, we need to explain how we can associate a Kripke structure to the rewrite theory specified by a Maude system module M.

Kripke structures are the natural models for propositional temporal logic. Essentially, a Kripke structure is a (total) unlabeled transition system to which we have added a collection of unary state predicates on its set of states.

A binary relation R A × A on a set A is called total if and only if for each a A there is at least one a′∈ A such that (a,a) R. If R is not total, it can be made total by defining R = R ∪{(a,a) A2⁄∃a′∈ A (a,a) R}.

A Kripke structure is a triple A = (A,A,L) such that A is a set, called the set of states, A is a total binary relation on A, called the transition relation, and L : A-→P(AP) is a function, called the labeling function, associating to each state a A the set L(a) of those atomic propositions in AP that hold in the state a.

The semantics of LTL(AP) is defined by means of a satisfaction relation

A, a |= φ

between a Kripke structure A having AP as its atomic propositions, a state a A, and an LTL formula φ LTL(AP). Specifically, A,a|=φ holds if and only if for each path π Path(A)a the path satisfaction relation

A, π |= φ

holds, where we define the set Path(A)a of computation paths starting at state a as the set of functions of the form π : ℕ - → A  such that π(0) = a and, for each n , we have π(n) →A π(n + 1).

We can define the path satisfaction relation (for any path, beginning at any state) inductively as follows:

How can we associate a Kripke structure to the rewrite theory R = (Σ,E,ϕ,R) specified by a Maude system module M? We just need to make explicit two things:

In general, the state predicates need not be part of the system specification and therefore they need not be specified in our system module M. They are typically part of the property specification. This is because the state predicates need not be related to the operational semantics of M: they are just certain predicates about the states of the system specified by M that are needed to specify some properties.

Therefore, after choosing a given kind, say [Foo], in M as our kind for states we can specify the relevant state predicates in a module M-PREDS protecting M according to the following general pattern:

  mod M-PREDS is  
    protecting M .  
    including SATISFACTION .  
    subsort Foo < State .  

where the dots ‘...’ indicate the part in which the syntax and semantics of the relevant state predicates are specified, as further explained in what follows.

The module SATISFACTION (contained in the model-checker.maude file) is very simple, and has the following specification:

  fmod SATISFACTION is  
    protecting BOOL .  
    sorts State Prop .  
    op _|=_ : State Prop -> Bool [frozen] .  

where the sorts State and Prop are unspecified. However, by importing SATISFACTION into M-PREDS and giving the subsort declaration

  subsort Foo < State .

all terms of sort Foo in M are also made terms of sort State. Note that we then have the kind identity [Foo] = [State].

The operator

  op _|=_ : State Prop -> Bool [frozen] .

is crucial to define the semantics of the relevant state predicates in M-PREDS. Each such state predicate is declared as an operator of sort Prop. In standard LTL propositional logic, the set AP of atomic propositions is assumed to be a set of constants. In Maude, however, we can define parametric state predicates, that is, operators of sort Prop which need not be constants, but may have one or more sorts as parameter arguments. We then define the semantics of such state predicates (when the predicate holds) by appropriate equations.

We can illustrate all this by means of a simple mutual exclusion example. Suppose that our original system module M is the following module MUTEX, in which two processes, one named a and another named b, can be either waiting or in their critical section, and take turns accessing their critical section by passing each other a different token (either $ or *).

  mod MUTEX is  
    sorts Name Mode Proc Token Conf .  
    subsorts Token Proc < Conf .  
    op none : -> Conf [ctor] .  
    op __ : Conf Conf -> Conf [ctor assoc comm id: none] .  
    ops a b : -> Name [ctor] .  
    ops wait critical : -> Mode [ctor] .  
    op [_,_] : Name Mode -> Proc [ctor] .  
    ops * $ : -> Token [ctor] .  
    rl [a-enter] : $ [a, wait] => [a, critical] .  
    rl [b-enter] : * [b, wait] => [b, critical] .  
    rl [a-exit] : [a, critical] => [a, wait] * .  
    rl [b-exit] : [b, critical] => [b, wait] $ .  

Our obvious kind for states is the kind [Conf] of configurations. In order to state the desired safety and liveness properties we need state predicates telling us whether a process is waiting or is in its critical section. We can make these predicates parametric on the name of the process and define their semantics as follows:

  mod MUTEX-PREDS is  
    protecting MUTEX .  
    including SATISFACTION .  
    subsort Conf < State .  
    op crit : Name -> Prop .  
    op wait : Name -> Prop .  
    var N : Name .  
    var C : Conf .  
    var P : Prop .  
    eq [N, critical] C |= crit(N) = true .  
    eq [N, wait] C |= wait(N) = true .  
    eq C |= P = false [owise] .  

Note the equations, defining when each of the two parametric state predicates holds in a given state.

The above example illustrates a general method by which desired state predicates for a module M are defined in a protecting extension, say M-PREDS, of M which imports SATISFACTION. One specifies the desired states by choosing a sort in M and declaring it as a subsort of State. One then defines the syntax of the desired state predicates as operators of sort Prop, and defines their semantics by means of a set of equations that specify for what states a given state predicate evaluates to true. We assume that those equations, when added to those of M, are (ground) Church-Rosser and terminating, and, furthermore, that M’s equational part is protected when the new operators and equations defining the state predicates are added.

Since we should protect BOOL, it is important to make sure that satisfaction of state predicates is fully defined. This can be checked with Maude’s Sufficient Completeness Checker (SCC) tool. This means that we should give equations for when the predicates are true and when they are false. In practice, however, this can often be reduced to specifying when a predicate is true by means of (possibly conditional) equations of the general form,

t |= p(v1,...,vn) = true if C

because we can use the owise feature (described in Section 4.5.4) to cover all the remaining cases, when it is false, with an equation

x : State |= p(y ,...,y ) = false [owise].
             1     n

In some cases, however—for example, because we want to perform reasoning using formal tools which do not accept owise declarations—we may fully define the true and false cases of a predicate not by using the owise attribute, but by explicit (possibly conditional) equations of the more general form,

t |= p(v1,...,vn) = bexp  if C,

where bexp is an arbitrary Boolean expression.

We are now ready to associate with a system module M specifying a rewrite theory R = (Σ,E,ϕ,R) (with a selected kind k of states and with state predicates Π defined by means of equations D in a protecting extension M-PREDS) a Kripke structure whose atomic predicates are specified by the set

AP Π = {θ(p) | p ∈ Π, θ ground substitution},

where by convention we use the simplified notation θ(p) to denote the ground term θ(p(x1,,xn)). This defines a labeling function LΠ on the set of states TΣ∕E,k assigning to each [t] TΣ∕E,k the set of atomic propositions

LΠ([t]) = {θ(p) ∈ APΠ | (E ∪D ) ⊢ (∀ ∅) t |= θ(p) = true}.

The Kripke structure we are interested in is then

                    1 ∙
K (R, k)Π = (TΣ∕E,k,(→ R ),LΠ ),

where (R1) denotes the total relation extending the one-step R-rewriting relation R1 among states of kind k, that is, [t] R1[t] holds if and only if there are u [t] and u′∈ [t] such that uis the result of applying one of the rules in R to u at some position. Under the usual assumptions that E is (ground) Church-Rosser and terminating (possibly modulo some axioms A contained in E) and R is (ground) coherent relative to E (again, possibly modulo A), u can always be chosen to be the canonical form of t under the equations E.

10.3 LTL model checking

Suppose that, given a system module M specifying a rewrite theory R = (Σ,E,ϕ,R), we have:

Then, as explained in Section 10.2, this defines a Kripke structure K(R,k)Π on the set of atomic propositions APΠ. Given an initial state [t] TΣ∕E,k and an LTL formula φ LTL(APΠ) we would like to have a procedure to decide the satisfaction relation

K(R,k)Π,[t] |= φ.

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

the set of states in TΣ∕E,k that are reachable from [t] by rewriting is finite,1 and
the rewrite theory R = (Σ,E,ϕ,R) specified by M plus the equations D defining the predicates Π are such that:

Under these assumptions, both the state predicates Π and the transition relation R1 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 [21]. The basis of this procedure is the following. Each LTL formula φ has an associated Büchi automaton Bφ whose acceptance ω-language is exactly that of the behaviors satisfying φ. We can then reduce the satisfaction problem

K(R, k) ,[t] |= φ

to the emptiness problem of the language accepted by the synchronous product of B¬φ and (the Büchi automaton associated with) (K(R,k)Π,[t]). The formula φ 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 [21]; and for a discussion of the specific techniques used in the Maude LTL model-checker implementation, see [57].

This makes clear our interest in obtaining the negative normal form of a formula ¬φ, since we need it to build the Büchi automaton B¬φ. For efficiency purposes we need to make B¬φ 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 ¬φ in the hope of generating a smaller Büchi automaton B¬φ. 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¬φ.

  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 .  

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  

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 (...)] .  

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] .  

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 φ is not satisfied by a finite Kripke structure, it is always possible to find a counterexample for φ having the form of a path of transitions followed by a cycle [21]. 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:

    including MODEL-CHECKER .  
    extending LTL .  
    sort Foo .  
    op a : -> Foo .  
    op f : Foo -> Foo .  
    rl a => f(a) .  
    subsort Foo < State .  
    op p : -> Prop .  

This module describes an infinite transition system of the form

a → f(a) → f(f(a)) → f(f(f(a))) → ⋅⋅⋅,

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.

10.4 The LTL satisfiability and tautology checker

A formula φ LTL(AP) is satisfiable if there is a Kripke structure A = (A,A,L), with L : A-→P(AP), and a computation path π such that A|=φ. Satisfiability of a formula φ LTL(AP) is a decidable property. In Maude, the satisfiability decision procedure is supported by the following predefined functional module SAT-SOLVER (also in the file model-checker.maude).

  fmod SAT-SOLVER is  
    protecting LTL .  
    *** formula lists and results  
    sorts FormulaList SatSolveResult TautCheckResult .  
    subsort Formula < FormulaList .  
    subsort Bool < SatSolveResult TautCheckResult .  
    op nil : -> FormulaList [ctor] .  
    op _;_ : FormulaList FormulaList -> FormulaList  
         [ctor assoc id: nil] .  
    op model : FormulaList FormulaList -> SatSolveResult [ctor] .  
    op satSolve : Formula ~> SatSolveResult [special (...)] .  
    op counterexample :  
         FormulaList FormulaList -> TautCheckResult [ctor] .  
    op tautCheck : Formula ~> TautCheckResult .  
    op $invert : SatSolveResult -> TautCheckResult .  
    var F : Formula .  
    vars L C : FormulaList .  
    eq tautCheck(F) = $invert(satSolve(~ F)) .  
    eq $invert(false) = true .  
    eq $invert(model(L, C)) = counterexample(L, C) .  

One can define the desired atomic predicates in a module extending SAT-SOLVER, such as, for example,

  fmod SAT-SOLVER-TEST is  
    extending SAT-SOLVER .  
    extending LTL .  
    ops a b c d e p q r : -> Formula .  

The user can then decide the satisfiability of an LTL formula involving those atomic propositions by applying the operator satSolve (whose special attribute has also been omitted in the module above) to the given formula and evaluating the expression. The resulting solution of sort SatSolveResult is then either false, if no model exists, or a finite model satisfying the formula. Such a model is described by a comma-separated pair of finite paths of states: an initial path leading to a cycle. Each state is described by a conjunction of atomic propositions or negated atomic propositions, with the propositions not mentioned in the conjunction being “don’t care” ones. For example, we can evaluate

  Maude> red satSolve(a /\ (O b) /\ (O O ((~ c) /\ [](c \/ (O c))))) .  
  reduce in SAT-SOLVER-TEST :  
    satSolve(O O (~ c /\ [](c \/ O c)) /\ (a /\ O b)) .  
  result SatSolveResult: model(a ; b, (~ c) ; c)

which is satisfied by a four-state model with a holding in the first state, b holding in the second, c not holding in the third but holding in the fourth, and the fourth state going back to the third, as shown in Figure 10.2.


Figure 10.2: Graphical representation of a Kripke structure

We call φ LTL(AP) a tautology if and only if A,a|=LTLφ holds for every Kripke structure A = (A,A,L) with L : A-→P(AP), and every state a A. It then follows easily that φ is a tautology if and only if ¬φ is unsatisfiable. Therefore, the module SAT-SOLVER can also be used as a tautology checker. This is accomplished by using the tautCheck, $invert, and counterexample operators and their corresponding equations in SAT-SOLVER. The tautCheck function returns either true if the formula is a tautology, or a finite model that does not satisfy the formula. For example, we can evaluate:

  Maude> red tautCheck((a => (O a)) <-> (a => ([] a))) .  
  reduce in SAT-SOLVER-TEST : tautCheck((a => O a) <-> a => []a) .  
  result Bool: true  
  Maude> red tautCheck((a -> (O a)) <-> (a -> ([] a))) .  
  reduce in SAT-SOLVER-TEST : tautCheck((a -> O a) <-> a -> []a) .  
  result TautCheckResult: counterexample(a ; a ; (~ a), True)

The tautology checker gives us also a decision procedure for semantic LTL equality, which is further discussed in [57].

10.5 Other model-checking examples

In [26, Section 16.6] some properties of a Mobile Maude application are model checked. This example is interesting because two levels of reflection (see Chapter 11) are involved: the object level, at which Mobile Maude system code executes, and the metalevel, at which application code is executed.

The model checker can also be executed in Full Maude. This is illustrated with an example in Section 17.7. This example, though quite simple, is interesting in several ways. The use of parameterization is exploited at both the system and the property level. At the system level, it allows a succinct specification of a parametric system. At the property level, it makes possible the specification of the relevant properties for each value of the parameter, also in a very succinct way. This is quite useful, because the property formulas vary as the parameter changes, and the parametric description encompasses an infinite number of instance formulas.