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' \in A$ such that $(a,a') \in R$. If $R$ is not total, it can be made total by defining $R^{\bullet}=R \cup \{(a,a)\in A^{2} \mid \not\exists a' \in A \; (a,a')\in R \}$.

A Kripke structure is a triple $\mathcal{A}=(A,\rightarrow_{\mathcal{A}},L)$ such that $A$ is a set, called the set of states, $\rightarrow_{\mathcal{A}}$ is a total binary relation on $A$, called the transition relation, and $L: A \longrightarrow \mathcal{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 $\textrm{LTL}(AP)$ is defined by means of a satisfaction relation

$$\mathcal{A},a \models \varphi$$

between a Kripke structure $\mathcal{A}$ having $AP$ as its atomic propositions, a state $a \in A$, and an LTL formula $\varphi \in \textrm{LTL}(AP)$. Specifically, $\mathcal{A},a \models \varphi$ holds if and only if for each path $\pi \in Path(\mathcal{A})_{a}$ the path satisfaction relation

$$\mathcal{A},\pi \models \varphi$$

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

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

• We always have $\mathcal{A},\pi \models_{LTL} \top$.
• For $p \in AP$,
  
  $$\mathcal{A},\pi \models_{LTL} p \;\;\;\; \Leftrightarrow \;\;\;\; p \in L(\pi(0)).$$
  
  

• For $\bigcirc \varphi \in \textrm{LTL}(A)$,
  
  $$\mathcal{A},\pi \models_{LTL} \bigcirc \varphi \;\;\;\; \Leftrightarrow \;\;\;\; \mathcal{A},s;\pi \models_{LTL} \varphi,$$
  
  
  where $s: \mathbb{N}\longrightarrow \mathbb{N}$ is the successor function, and where $(s;\pi)(n) = \pi(s(n)) = \pi(n+1)$.
• For $\varphi \; \mathcal{U} \; \psi \in \textrm{LTL}(\mathcal{A})$,
  
  $$\mathcal{A},\pi \models_{LTL} \varphi \; \mathcal{U} \; \psi \;\;\;\; \Leftrightarrow$$
  
  
  
  
  $$(\exists n \in \mathbb{N})$$
  
  
  
  
  $$\;\;\;\;\;(( \mathcal{A},s^{n};\pi \models_{LTL} \psi) \wedge... ...n \; \Rightarrow \mathcal{A},s^{m};\pi \models_{LTL} \varphi)).$$
  
  

• For $\neg \varphi \in \textrm{LTL}(AP)$,
  
  $$\mathcal{A},\pi \models_{LTL} \neg \varphi \;\;\;\; \Leftrightarrow \;\;\;\; \mathcal{A}, \pi \not\models_{LTL} \varphi.$$
  
  

• For $\varphi \vee \psi \in \textrm{LTL}(AP)$,
  
  $$\mathcal{A},\pi \models_{LTL} \varphi \vee \psi \;\;\;\; \Lef... ...i \; \;\; \mbox{or} \; \;\; \mathcal{A},\pi \models_{LTL} \psi.$$
  
  

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

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

$$t \models p(v_{1},\ldots,v_{n}) = true \;\; \textit{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:\mathit{State} \models p(y_{1},\ldots,y_{n}) = \mathit{false} \;\; \texttt{[owise]} .$$

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 \models p(v_{1},\ldots,v_{n}) = bexp \;\; \textit{if} \;\; C,$$

where $bexp$ is an arbitrary Boolean expression.

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

$$AP_{\Pi} = \{ \theta(p) \mid p \in \Pi, \; \theta \; \mbox{ground substitution}\},$$

where by convention we use the simplified notation $\theta(p)$ to denote the ground term $\theta(p(x_{1},\ldots,x_{n}))$. This defines a labeling function $L_{\Pi}$ on the set of states $T_{\Sigma/E,k}$ assigning to each $[t] \in T_{\Sigma/E,k}$ the set of atomic propositions

$$L_{\Pi}([t]) = \{\theta(p)\in AP_{\Pi} \mid (E \cup D) \vdash \;(\forall \; \emptyset)\; t \models \theta(p) = true\}.$$

The Kripke structure we are interested in is then

$$\mathcal{K}({\cal R},k)_{\Pi}=(T_{\Sigma/E,k}, (\rightarrow^{1}_{{\cal R}})^{\bullet},L_{\Pi}),$$

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