Chapter 10
LTL Model Checking

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

• a system specification level, provided by the rewrite theory specified by that system module which defines the behavior of the system, and
• a property specification level, given by some property (or properties) φ that we want to state and prove about our module.

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 [16]; we focus on linear temporal logic [73, 16], 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:

• True: ⊤ LTL(AP).
• Atomic propositions: If p AP, then p LTL(AP).
• Next operator: If φ LTL(AP), then ○φ LTL(AP).
• Until operator: If φ,ψ LTL(AP), then φ ψ LTL(AP).
• Boolean connectives: If φ,ψ LTL(AP), then the formulas ¬φ, and φ ∨ ψ are in LTL(AP).

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

• Other Boolean connectives:
  • False: ⊥ = ¬⊤
  • Conjunction: φ ∧ ψ = ¬((¬φ) ∨ (¬ψ))
  • Implication: φ → ψ = (¬φ) ∨ ψ.
• Other temporal operators:
  • Eventually: ◊φ = ⊤ φ
  • Henceforth: □φ = ¬◊¬φ
  • Release: φ ψ = ¬((¬φ) (¬ψ))
  • Unless: φ ψ = (φ ψ) ∨ (□φ)
  • Leads-to: φ ↝ ψ = □(φ → (◊ψ))
  • Strong implication: φ ⇒ ψ = □(φ → ψ)
  • Strong equivalence: φ ⇔ ψ = □(φ ↔ ψ).

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

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 ⊤, ○, , and ∨ (respectively, True, O_, _U_, and _\/_) as constructors. That is, we need to also have as constructors the dual connectives: ⊥, , 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) A²∣⁄∃a′ A (a,a′) R}.

A Kripke structure is a triple = (A,→,L) such that A is a set, called the set of states, → is a total binary relation on A, called the transition relation, and L : A-→(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

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

holds, where we define the set Path()_a of computation paths starting at state a as the set of functions of the form such that π(0) = a and, for each n ℕ, we have

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

• We always have ,π_LTL⊤.
• For p AP,

• For ○φ LTL(A),

  where s : ℕ-→ℕ is the successor function, and where (s;π)(n) = π(s(n)) = π(n + 1).

• For φ ψ LTL(),
  
  

• For ¬φ LTL(AP),

• For φ ∨ ψ LTL(AP),

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

• the intended kind k of states in the signature Σ, and
• the relevant state predicates, that is, the relevant set AP of atomic propositions.

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:

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:

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

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

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 *).

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:

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,

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

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,

where bexp is an arbitrary Boolean expression.

We are now ready to associate with a system module M specifying a rewrite theory = (Σ,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

where by convention we use the simplified notation θ(p) to denote the ground term θ(p(x₁,…,x_n)). 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

The Kripke structure we are interested in is then

where (→¹)^∙ denotes the total relation extending the one-step -rewriting relation →¹ among states of kind k, that is, [t] →¹[t′] holds if and only if there are u [t] and u′ [t′] such that u′ is 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 = (Σ,E,ϕ,R), we have:

• chosen a kind k in M as our kind of states;
• defined some state predicates Π 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 (,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

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

1. the set of states in T_Σ∕E,k that are reachable from [t] by rewriting is finite,¹ and
2. the rewrite theory = (Σ,E,ϕ,R) specified by M plus the equations D defining the predicates Π are such that:
   • both E and E ∪ D are (ground) Church-Rosser and terminating, perhaps modulo some axioms A, with (Σ,E) ⊆ (Σ ∪ Π,E ∪ 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 Π and the transition relation →¹ 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 [16]. 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

to the emptiness problem of the language accepted by the synchronous product of B_¬φ and (the Büchi automaton associated with) ((,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 [16]; and for a discussion of the specific techniques used in the Maude LTL model-checker implementation, see [48].

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_¬φ.

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:

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:

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

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.

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

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:

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:

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

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 [16]. 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:

This module describes an infinite transition system of the form

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

we run into a nonterminating computation.

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

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,→,L), with L : A-→(AP), and a computation path π such that ,πφ. 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).

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

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

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.

We call φ LTL(AP) a tautology if and only if ,a_LTLφ holds for every Kripke structure = (A,→,L) with L : A-→(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:

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

10.5 Other model-checking examples

In [21, 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.