Chapter 12
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) $\phi$ 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. In Section 12.6 we consider a simple, but useful, extension of LTL that we call LTL+ and whose model checking is also supported by 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 [19]; we focus on linear temporal logic [85, 19], because of its intuitive appeal, widespread use, and well-developed proof methods and decision procedures.

12.1 LTL formulas and the LTL module

Given a set $AP$ of atomic propositions, we define the formulas of the propositional linear temporal logic $\mathrm{\text{LTL}}(AP)$ inductively as follows:

• True: $\top <!--FUNCTION\; APPLICATION-->\in \mathrm{\text{LTL}}(AP)$.

• Atomic propositions: If $p\in AP$, then $p\in \mathrm{\text{LTL}}(AP)$.

• Next operator: If $\phi \in \mathrm{\text{LTL}}(AP)$, then $○\phi \in \mathrm{\text{LTL}}(AP)$.

• Until operator: If $\phi ,\psi \in \mathrm{\text{LTL}}(AP)$, then $\phi U\psi \in \mathrm{\text{LTL}}(AP)$.

• Boolean connectives: If $\phi ,\psi \in \mathrm{\text{LTL}}(AP)$, then the formulas $\neg <!--FUNCTION\; APPLICATION-->\phi$, and $\phi \vee \psi$ 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: $\perp =\neg <!--FUNCTION\; APPLICATION-->\top <!--FUNCTION\; APPLICATION-->$

  • Conjunction: $\phi \wedge \psi =\neg <!--FUNCTION\; APPLICATION-->((\neg <!--FUNCTION\; APPLICATION-->\phi )\vee (\neg <!--FUNCTION\; APPLICATION-->\psi ))$

  • Implication: $\phi \to \psi =(\neg <!--FUNCTION\; APPLICATION-->\phi )\vee \psi$.

• Other temporal operators:

  • $\text{Eventually:}◇\phi =\top <!--FUNCTION\; APPLICATION-->U\phi$

  • $\text{Henceforth:}\square \phi =\neg <!--FUNCTION\; APPLICATION-->◇\neg <!--FUNCTION\; APPLICATION-->\phi$

  • $\text{Release:}\phi R\psi =\neg <!--FUNCTION\; APPLICATION-->((\neg <!--FUNCTION\; APPLICATION-->\phi )U(\neg <!--FUNCTION\; APPLICATION-->\psi ))$

  • $\text{Unless:}\phi W\psi =(\phi U\psi )\vee (\square \phi )$

  • $\text{Leads-to:}\phi \rightsquigarrow \psi =\square (\phi \to (◇\psi ))$

  • $\text{Strong implication:}\phi \Rightarrow \psi =\square (\phi \to \psi )$

  • $\text{Strong equivalence:}\phi \iff \psi =\square (\phi \leftrightarrow \psi )$.

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

                                                                              
     

Note that, for the moment, no set $AP$ of atomic propositions has been specified in the LTL module. Section 12.2 explains how such atomic propositions are defined for a given system module M, and Section 12.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 $\top <!--FUNCTION\; APPLICATION-->,○,U$, and $\vee$ (respectively, True, O_, _U_, and _\/_) as constructors. That is, we need to also have as constructors the dual connectives: $\perp ,R$, and $\wedge$ (respectively, False, _R_, and _/\_). Note that $○$ is self-dual.

12.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\subseteq A\times A$ on a set $A$ is called total if and only if for each $a\in A$ there is at least one $a^{\prime }\in A$ such that $(a,a^{\prime })\in R$. If $R$ is not total, it can be made total by defining $R^{\bullet }=R\cup \{(a,a)\in A^2\mid \nexists a^{\prime }\in A(a,a^{\prime })\in R\}$.

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

The semantics of $\mathrm{\text{LTL}}(AP)$ is defined by means of a satisfaction relation

between a Kripke structure $A$ having $AP$ as its atomic propositions, a state $a\in A$, and an LTL formula $\phi \in \mathrm{\text{LTL}}(AP)$. Specifically, $A,a\vDash \phi$ holds if and only if for each path $\pi \in Path{(A)}_a$ the path satisfaction relation

holds, where we define the set $Path{(A)}_a$ of computation paths starting at state $a$ as the set of functions of the form $\pi :\mathbb{N}\to A$ such that $\pi (0)=a$ and, for each $n\in \mathbb{N}$, we have $\pi (n){\to }_A\pi (n+1).$

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

• We always have $A,\pi {\vDash }_{LTL}\top <!--FUNCTION\; APPLICATION-->$.

• For $p\in AP$,

  $$A,\pi {\vDash }_{LTL}p\iff p\in L(\pi (0)).$$

• For $○\phi \in \mathrm{\text{LTL}}(A)$,

  $$A,\pi {\vDash }_{LTL}○\phi \iff A,s;\pi {\vDash }_{LTL}\phi ,$$

  where $s:\mathbb{N}\to \mathbb{N}$ is the successor function, and where $(s;\pi )(n)=\pi (s(n))=\pi (n+1)$.

• For $\phi U\psi \in \mathrm{\text{LTL}}(A)$,

  $$A,\pi {\vDash }_{LTL}\phi U\psi \iff$$

  $$(\exists <!--FUNCTION\; APPLICATION-->n\in \mathbb{N})$$

  $$((A,s^n;\pi {\vDash }_{LTL}\psi )\wedge ((\forall <!--FUNCTION\; APPLICATION-->m\in \mathbb{N})m<n\Rightarrow A,s^m;\pi {\vDash }_{LTL}\phi )).$$

• For $\neg <!--FUNCTION\; APPLICATION-->\phi \in \mathrm{\text{LTL}}(AP)$,

  $$A,\pi {\vDash }_{LTL}\neg <!--FUNCTION\; APPLICATION-->\phi \iff A,\pi {⊭}_{LTL}\phi .$$

• For $\phi \vee \psi \in \mathrm{\text{LTL}}(AP)$,

  $$A,\pi {\vDash }_{LTL}\phi \vee \psi \iff A,\pi {\vDash }_{LTL}\phi \text{or}A,\pi {\vDash }_{LTL}\psi .$$

How can we associate a Kripke structure to the rewrite theory $R=(\mathrm{\Sigma },E,\varphi ,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 $\mathrm{\Sigma }$, 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:

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

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

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 $\mathtt{\text{[Foo]}}=\mathtt{\text{[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.

Note that the operator _|=_ is declared as partial, using ~> (see Section 3.5). As we will see below, a user is only required to ensure that it reduces to true in the positive case(s) and it can return anything in the negative cases. Declaring it to be partial means that it returns a result in the kind [Bool] rather than sort Bool, thus protecting BOOL, as it is declared in the module SATISFACTION.

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

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

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 $R=(\mathrm{\Sigma },E,\varphi ,R)$ (with a selected kind $k$ of states and with state predicates $\mathrm{\Pi }$ 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_1,\dots ,x_n))$. This defines a labeling function $L_{\mathrm{\Pi }}$ on the set of states $T_{\mathrm{\Sigma }∕E,k}$ assigning to each $[t]\in T_{\mathrm{\Sigma }∕E,k}$ the set of atomic propositions

The Kripke structure we are interested in is then

where ${({\to }_R^1)}^{\bullet }$ denotes the total relation extending the one-step $R$-rewriting relation ${\to }_R^1$ among states of kind $k$, that is, $[t]{\to }_R^1[t^{\prime }]$ holds if and only if there are $u\in [t]$ and $u^{\prime }\in [t^{\prime }]$ such that $u^{\prime }$ 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$.

12.3 LTL model checking

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

• chosen a kind $k$ in M as our kind of states;

• defined some state predicates $\mathrm{\Pi }$ and their semantics in a module, say M-PREDS, protecting M by the method already explained in Section 12.2.

Then, as explained in Section 12.2, this defines a Kripke structure $K{(R,k)}_{\mathrm{\Pi }}$ on the set of atomic propositions $A{P}_{\mathrm{\Pi }}$. Given an initial state $[t]\in T_{\mathrm{\Sigma }∕E,k}$ and an LTL formula $\phi \in LTL(A{P}_{\mathrm{\Pi }})$ 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_{\mathrm{\Sigma }∕E,k}$ that are reachable from $[t]$ by rewriting is finite,¹ and

2.

the rewrite theory $R=(\mathrm{\Sigma },E,\varphi ,R)$ specified by M plus the equations $D$ defining the predicates $\mathrm{\Pi }$ are such that:

• both $E$ and $E\cup D$ are (ground) Church-Rosser and terminating, perhaps modulo some axioms $A$, with $(\mathrm{\Sigma },E)\subseteq (\mathrm{\Sigma }\cup \mathrm{\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 $\mathrm{\Pi }$ and the transition relation ${\to }_R^1$ 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 [19]. The basis of this procedure is the following. Each LTL formula $\phi$ has an associated Büchi automaton $B_{\phi }$ whose acceptance $\omega$-language is exactly that of the behaviors satisfying $\phi$. We can then reduce the satisfaction problem

to the emptiness problem of the language accepted by the synchronous product of $B_{\neg <!--FUNCTION\; APPLICATION-->\phi }$ and (the Büchi automaton associated with) $(K{(R,k)}_{\mathrm{\Pi }},[t])$. The formula $\phi$ 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 [19]; and for a discussion of the specific techniques used in the Maude LTL model-checker implementation, see [53].

This makes clear our interest in obtaining the negative normal form of a formula $\neg <!--FUNCTION\; APPLICATION-->\phi$, since we need it to build the Büchi automaton $B_{\neg <!--FUNCTION\; APPLICATION-->\phi }$. For efficiency purposes we need to make $B_{\neg <!--FUNCTION\; APPLICATION-->\phi }$ 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 <!--FUNCTION\; APPLICATION-->\phi$ in the hope of generating a smaller Büchi automaton $B_{\neg <!--FUNCTION\; APPLICATION-->\phi }$. 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 <!--FUNCTION\; APPLICATION-->\phi }$.

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