The LTL satisfiability and tautology checker

A formula $\varphi \in \textrm{LTL}(AP)$ is satisfiable if there is a Kripke structure $\mathcal{A}=(A,\rightarrow_{\mathcal{A}},L)$, with $L: A \longrightarrow \mathcal{P}(AP)$, and a computation path $\pi$ such that $\mathcal{A},\pi \models \varphi.$ Satisfiability of a formula $\varphi \in \textrm{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) .
  endfm

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

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 $\varphi \in \textrm{LTL}(AP)$ a tautology if and only if $\mathcal{A},a \models_{\scriptscriptstyle LTL} \varphi$ holds for every Kripke structure $\mathcal{A}=(A,\rightarrow_{\mathcal{A}},L)$ with $L: A \longrightarrow \mathcal{P}(AP)$, and every state $a \in A$. It then follows easily that $\varphi$ is a tautology if and only if $\neg \varphi$ 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 [39].