Model checking strategy-controlled systems in rewriting logic

Abstract

Rewriting logic and its implementation Maude are an expressive framework for the formal specification and verification of software and other kinds of systems. Concurrency is naturally represented by nondeterministic local transformations produced by the application of rewriting rules over algebraic terms in an equational theory. Some aspects of the global behavior of the systems or additional constraints sometimes require restricting this nondeterminism. Rewriting strategies are used as a higher-level and modular resource to cleanly capture these requirements, which can be easily expressed in Maude with an integrated strategy language. However, strategy-aware specifications cannot be verified with the builtin LTL model checker, making strategies less useful and attractive. In this paper, we discuss model checking for strategy-controlled systems, and present a strategy-aware extension of the Maude LTL model checker. The expressivity of the strategy language is discussed in relation to model checking, the model checker is illustrated with multiple application examples, and its performance is compared.

Proofs

Proposition 1

Given $E \subseteq S^\omega$, there is a finite Kripke structure ${\mathscr {K}}'$ such that $\ell (\varGamma ^\omega _{{\mathscr {K}}'}) = \ell (E)$ iff $\ell (E)$ is closed and $\omega$-regular.

Proof

Notice that the finite Kripke structure ${\mathscr {K}}'$ can act as Büchi automaton and vice versa. Given a Kripke structure $(S, \rightarrow , I, AP, \ell )$, the automaton $(S \cup \{\iota \}, {\mathscr {P}}(AP), \delta , \iota , S \cup \{\iota \})$ with $\delta (\iota , P) = \{ s \in I : \ell (s) = P \}$ and $\delta (s, P) = \{ s' \in S : \ell (s') = P \;\wedge \; s \rightarrow s' \}$ is considered; and given an automaton $(Q, {\mathscr {P}}(AP), \delta , q_0, F)$, we consider the Kripke structure $(Q \times {\mathscr {P}}(AP), \rightarrow , \{ (s, \ell (s)) : s_0 \rightarrow s, s_0 \in I \}, AP, \pi _2)$ with $(s, P) \rightarrow (s', P')$ if $s \rightarrow s'$ and $\ell (s') = P'$. Checking that their word and execution coincides is straightforward, taking into account that E is closed and so F is irrelevant. $\square$

Proposition 2

The projection of the infinite traces of ${\mathscr {M}}_{\alpha , t}$ by $\pi _1 \circ \mathrm {cterm}$ coincides with the stuttering-extension of $E(\alpha , t)$.

Proof

Remember that ${\mathscr {M}}_{\alpha , t}$ is defined as $(\mathscr {X\!S}\times \{0\} \cup \mathrm {Sol}\times \{1\}, \twoheadrightarrow _\mathrm {Sol})$ where $(q, 0) \twoheadrightarrow _\mathrm {Sol}(q', 0)$ if $q \twoheadrightarrow q'$ and $(q, k) \twoheadrightarrow _\mathrm {Sol}(q, 1)$ if $q \in \mathrm {Sol}$ for $k=0,1$. Consequently, all infinite traces of ${\mathscr {O}}$ are infinite traces of ${\mathscr {M}}_{\alpha , t}$ (with a zero in the second component), but these are exactly $\mathrm {Ex}^\omega (\alpha , t)$ by definition. The finite traces $q_1 \cdots q_n$ in ${\mathscr {O}}$ are finite traces $(q_1, 0) \cdots (q_n, 0)$ in ${\mathscr {M}}_{\alpha , t}$, but if and only if $q_n \in \mathrm {Sol}$ they can be extended to the infinite traces $(q_1, 0) \cdots (q_n, 0) (q_n, 1) \cdots$. These are the traces in $\mathrm {Ex}^*(\alpha , t)$, whose stuttering-extended projections in $E(\alpha , t)$ are precisely $\mathrm {cterm}(q_1) \cdots \mathrm {cterm}(q_n) \, \mathrm {cterm}(q_n) \cdots$, the projection of the extended executions ending in a halting state. Thus, $\mathrm {cterm}(\pi _1(\varGamma ^\omega _{{\mathscr {M}}_{\alpha , t}}))$ is the stuttering-extension of $E(\alpha , t)$, where $\pi _1(x, y) = x$. $\square$

Lemma 1

If the underlying equational theory is decidable and the reachable states from $t \,\hbox {@}\,\alpha$ are finitely many, $\twoheadrightarrow$ and $\rightarrow _{s,c}$ are decidable.

Proof

All the rules defining $\rightarrow _c$ and $\rightarrow _s$ but [else] are decidable, since they only involve immediate term manipulations, matching, substitution application, etc. The [else] rule is decidable on an execution state $t \,\hbox {@}\,{ \,\beta \, \texttt {?} \,\gamma \, \texttt {:} \,\zeta }s$ if the reachable states from $t \,\hbox {@}\,\beta \, \mathrm {vctx}(s)$ are finitely many. However, these are already embedded in the states reachable from the conditional, since $t \,\hbox {@}\,{ \,\beta \, \texttt {?} \,\gamma \, \texttt {:} \,\zeta }s \rightarrow _c t \,\hbox {@}\,\beta \gamma s$ and all the successors of $t \,\hbox {@}\,\beta \, \mathrm {vctx}(s)$ are successors of $t \,\hbox {@}\,\beta \gamma s$ with $\mathrm {vctx}(s)$ replaced by $\gamma s$, since the same rules can be applied with their free variables s changed like this. In case of nested conditionals, this argument can be repeated from inside out conditional expressions, so all these states are reachable from the initial $t \,\hbox {@}\,\alpha$, and so they are finitely many and the rule is decidable. Since the reachable states are a finite set, deciding $q \twoheadrightarrow q'$ is finding a path via $\rightarrow _c$ transitions from q to any predecessor of $q'$ by a $\rightarrow _s$ transition, so it is decidable. $\square$

Proposition 3

For any $\infty$-recursively enumerable language $L \subseteq \varGamma _{{\mathscr {M}}}$, there is some strategy expression $\alpha$ such that $E(\alpha ) = L$.

Proof

The finite-word part $L_*$ and the infinite-word part $L_\omega$ of L can be considered separately. In effect, if there is a strategy expression $\alpha$ such that $E(\alpha ) = L_*$ and a strategy expression $\beta$ such that $E(\beta ) = L_\omega$, then $E(\alpha { \texttt {|}}\beta ) = E(\alpha ) \cup E(\beta ) = L_* \cup L_\omega = L$.

Let us start with the finite-word part $L_*$. Since it is recursively enumerable, there must be a Turing machine $M = (Q, \varGamma , T_\varSigma , q_0, F, \delta )$ such that $L_* = L(M)$. Turing machines can easily be represented in Maude, but for the sake of brevity we will see them as terms with two defined operators: accept that evaluates to true if the word in its tape is accepted, and append that puts a symbol on its tape. A generic specification including these functions is available at (Eker et al. 2021). The strategy that admits exactly $L_*$ is defined as a recursive expression that carries a Turing machine as an argument and fills the tape with the visited terms while rewriting. At some point, it runs the Turing machine to decide if the accumulated word is accepted and can be yielded as a solution of the strategy.

The initial strategy call is climb(M0, 0) where M0 is in its initial state with an empty tape. Observe that this nonterminating strategy climb fixes in advance the length of the executions to be recognized by run. This is a technical detail to avoid admitting infinite executions that are accumulation points of the finite words in the language. We claim that run(M0, n) admits all words in $L_*$ of length n. In effect, the contents of the tape of M is the sequence of terms visited until but not including the current subject term S. If the second argument is positive, the current state is appended to the tape by append(M, S), a new rewrite step is performed, hence maintaining the invariant in the previous phrase, and run is called with $n-1$. If the counter is zero, the Turing machine M is executed by accept(M’) after appending the last state S, which only evaluates to true if the word or execution in its tape is in $L_*$, and only in this case the strategy yields a solution. Finally, the strategy climb clearly admits the union of all executions allowed by run(M, n) for all $n \in {\mathbb {N}}$, which are all the bounded subsets of $L_*$, so it admits $L_*$. Moreover, it does not admit any other word since the infinite $\rightarrow _{s,c}$-execution repeating

$$\begin{aligned} t \,\hbox {@}\,\texttt {climb(M}, n\texttt {)} \rightarrow _c t \,\hbox {@}\,(\texttt {run(M}, n\texttt {) | climb(M}, n+1\texttt {)}) \rightarrow _c t \,\hbox {@}\,\texttt {climb(M,} n+1\texttt {)} \end{aligned}$$

does not contain a single system transition or $\twoheadrightarrow$ step. Naively, we could have defined the strategy as simply

However, while representing the language $L_* = \{t\}^*$ for some term t, the infinite repetition of t will be inevitably allowed because of the execution that always takes the second branch.

The case of $\omega$-languages is more complicated, but the proof is similar. We assume that the language $L_\omega$ is represented by a nondeterministic Turing machine with Büchi conditions and type 2 semantics (Finkel 2014). They are defined as tuples $M = (Q, \varSigma , \varGamma , \delta , F, q_0)$ where Q is a finite set of states, $\varSigma$ is a finite input alphabet (in our case, a subset of $T_\varSigma$), $\varGamma$ is a finite tape alphabet with $\varSigma \subseteq \varGamma$, F is a set of states to define the Büchi condition, $q_0 \in Q$ is the initial state, and $\delta : Q \times \varGamma \rightarrow {\mathscr {P}}(Q \times \varGamma \times \{L, R, S\})$ is the nondeterministic transition function. A run of M for a word w is an infinite sequence of configurations $r = (q_i, w_i, j_i)^\infty _{i=1}$ with $r_1 = (q_0, w, 0)$ and $r_{k+1} = (q_{k+1}, w_k[j_k/s], j_k + m)$ if $(q_{k+1}, s, m) \in \delta (q_k, (w_k)_{j_k})$ where m is $-1$ for L, 1 for R, and 0 for S. A run is complete if every position of the tape is eventually visited. A word is accepted if there is a run such that $q_i \in F$ infinitely often.

The climb definition is identical to the finite case, but now it fixes the next configuration where a final state of the Turing machine must be found, and it is called repeatedly to ensure that those are visited infinitely often. Since executing the Turing machine after writing an infinite word into the tape is not possible, we advance it while running the strategy and fill the tape lazily when required. When the machine moves right to a blank position, this is revealed by the needsInput predicate, a rewrite step is executed, and the new term is put in place of the blank before it can be read. Each step of the Turing machine consumes the counter and when it bumps into zero, the current state of the Turing machine is checked to be final. If it is not, the execution is discarded. Otherwise, a new call to climb ensures that a final state will be visited again.

Let $\alpha$ be climb(M0, 0). First, $E(\alpha ) \subseteq L(M)$. If $w \in E(\alpha )$, by definition of $E(\alpha )$ and $\twoheadrightarrow$, there must be some $(q_n)_{k=0}^\infty \in \mathscr {X\!S}^\omega$ and $(n_k)_{k=0}^\infty \in {\mathbb {N}}^\omega$ such that $q_n \rightarrow _{s,c} q_{n+1}$, $q_{n_k} \twoheadrightarrow q_{n_{k+1}}$ and $\mathrm {cterm}(q_{n_k}) = w_k$. The only rule application in the strategies involved is the all in the positive branch of the conditional of the second run definition. Hence, this branch must have been executed infinitely many times, and so the machine must have moved its head infinitely many times to positions of the tape that need input. The machine is moved only in the negative branch of the same definition by a strategy-call $\rightarrow _c$ transition, so let $(m_k)_{k=0}^\infty$ be the indices of the states followed by these transitions. Taking the argument M of these calls, a run $(c_k)_{k=0}^\infty$ of the Turing machine can be constructed. In effect, $c_k \vdash c_{k+1}$ by the meaning of step, the run is complete since it visits infinitely many positions of the tape, and so the entire tape since it moves only one cell at a time, and the contents of the tape is the word w since this is what put inserts each time a rule is executed. Moreover, the Büchi condition is satisfied because of the climb strategy: at any configuration $c_k$, the number of steps until a new final state is reached can be read from the second argument of the run call. In conclusion, $(c_k)_{k=0}^\infty$ is an accepting run of the machine, and so $(w_k)_{k=0}^\infty \in L(M)$.

To prove the converse $L(M) \subseteq E(\alpha )$, let $(c_k)_{k=0}^\infty$ be a complete and accepting run of the Turing machine for some word $w \in L_\omega$. Since it is accepting, it must visit infinitely many final states, and there exists $(n_k)_{k=0}^\infty$ with $n_k \ge 1$ such that $c_{n_k}$ is in a final state. Moreover, since the run is complete, all the positions of the tape must be visited, so there is a $(m_k)_{k=0}^\infty$ such that the machine visits the position k for the first time in $c_{m_k}$. With these ingredients, we can construct a nonterminating derivation of the operational semantics: starting at $q_0 = t_0 \,\hbox {@}\,\alpha$, climb calls run with $n_0$, and then the execution of run is deterministic until N reaches zero except for all and the selection of the move of the nondeterministic machine. Each time the second branch of the conditional has to be executed, we choose the next machine configuration $c_k$ in the run in the matchrew. Similarly, when the first branch is executed, the result of all is chosen to match the value of the current cell in $c_k$ and this is always possible since $(w_k)_{k=0}^\infty$ is a valid rewriting path of the uncontrolled system. When the counter descends to zero, the test in the run definition is satisfied, since the configuration is some final $c_{n_k}$, and the new run argument generated by climb is chosen to be $n_k - n_{k+1}$, and this procedure is repeated forever. The resulting $\rightarrow _{s,c}$ derivation contains infinitely many $\rightarrow _s$ transitions as a consequence of the completeness of the machine run, and so a $\twoheadrightarrow$ derivation can be extracted whose projection is the expected word w since the all outputs have been chosen to match it. Therefore, $w \in E(\alpha )$. $\square$

Proposition 4

If the reachable states from $t \,\hbox {@}\,\alpha$ are finitely many, $E(\alpha , t)$ is a closed $\infty$-regular language.

Proof

The Büchi automaton for $E(\alpha , t)$ is $A = (Q, \mathrm {cterm}(Q), \delta , \{\textit{start}\}, Q)$ where $Q = \{\textit{start}\} \cup \{ q \in \mathscr {X\!S}\mid t \,\hbox {@}\,\alpha \twoheadrightarrow ^* q \} \cup \{ t' \,\hbox {@}\,\varepsilon : t \,\hbox {@}\,\alpha \rightarrow _{s,c}^* t' \,\hbox {@}\,\varepsilon \}$ and

$$\begin{aligned} \delta (\textit{start}, t)&= \{\; t \,\hbox {@}\,\alpha \;\}& \\ \delta (\textit{start}, t')&= \emptyset&\text {if } t' \neq t \\ \delta (q, t')&= \{\; q' : q \twoheadrightarrow q' \;\wedge \; \mathrm {cterm}(q') = t' \;\}&\text {for } q \in Q \,\backslash \, \{\textit{start}\} \\&\quad \cup \{\; t' \,\hbox {@}\,\varepsilon : \text {if } q \rightarrow _c^* t' \,\hbox {@}\,\varepsilon \;\} \end{aligned}$$

The identity $L(A) = E(\alpha , t)$ follows from the fact that runs $\pi$ in A yield executions $\mathrm {cterm}(\pi )$ in $E(\alpha , t)$ and vice versa. Proving this is straightforward, on account of the definitions of A and $E(\alpha , t)$. The proof for finite words is identical. $\square$

Lemma 2

Given two terms $t,t' \in T_\varSigma$ such that $t \rightarrow ^1_R t'$, there is a strategy expression $\alpha _{t,t'}$ of the form $\texttt {matchrew} \; P \; \texttt {by} \; x \; \texttt {using} \; rl[\rho ]\{{\mathbf{\beta }}\} \; \texttt{;} \; \texttt{match} \; t'$ such that $t \,\hbox {@}\,\alpha _{t,t'} \rightarrow _{s,c}^* u \,\hbox {@}\,\varepsilon$ iff $t' = u$ and there are finitely many reachable states from $\alpha _{t,t'}$.

Proof

Notice that the much simpler strategy all ; match $t'$ also satisfies the first requirement, but not necessarily the second since the rewriting condition may have infinitely many solutions. If $t \rightarrow ^1_R t'$, there must exist a (perhaps conditional) rule $\textit{rl} : l \rightarrow r \; \mathrm {if}\; C$, a substitution $\sigma$, and a position p in t such that $t|_p = \sigma (l)$, $t' = t[p/\sigma (r)]$ and $\sigma (C)$ holds. Proceeding by induction on the number of rewriting conditions required to prove a step, we first suppose that C does not contain rewriting condition fragments. If $x_1, \ldots , x_n$ are the variables that occur in l and C, and x is a fresh variable, the desired $\alpha$ is then

$$\begin{aligned} \texttt {matchrew} \; t[p\,/\,x] \; \texttt {by} \; x \; \texttt {using} \; \textit{rl}\,[x_1 \leftarrow \sigma (x_1), \ldots , x_n \leftarrow \sigma (x_n)] \; \texttt{;} \; \texttt{match} \; t' \end{aligned}$$

This strategy forces the $\textit{rl}$ rule application to the specific position p, with the specific substitution $\sigma$. The only possible execution is

$$\begin{aligned} t \,\hbox {@}\,\alpha _{t,t'}&\rightarrow _c \mathrm {subterm}(x : t|_p \,\hbox {@}\,\textit{rl}\,[x_k \leftarrow \sigma (x_k)]_{k=1}^n; t[p\,/\,x]) \,\hbox {@}\;\texttt{match} \; t' \\&\rightarrow _s \mathrm {subterm}(x : \sigma (r) \,\hbox {@}\,\varepsilon ; t[p\,/\,x]) \,\hbox {@}\;\texttt{match} \; t' \rightarrow _c^* t' \,\hbox {@}\, \varepsilon \end{aligned}$$

If C contains rewriting conditions, we have to indicate strategies for these. Since $t \rightarrow ^1_R t'$, for each rewriting condition $l' \;\mathtt{=>}\;r'$, a sequence $t_1 t_2 \cdots t_n$ must exist with $\sigma (l') = t_1$, $\sigma (r') = t_n$ and $t_k \rightarrow ^1_R t_{k+1}$. Some of these steps may apply rules with rewriting conditions, but we are one level less, so the existence of $\alpha _{t_k, t_{k+1}}$ can be assumed. Joining all the transitions with the concatenation operator of strategies, a strategy is built to solve one of the rewriting conditions. The same can be done for the other rewriting fragments, so the lemma holds. $\square$

Proposition 5

If L is a closed $\infty$-regular language, there is a strategy expression $\beta$ such that $E(\beta ) = L$ and the reachable states from $t \,\hbox {@}\,\beta$ are finitely many for all $t \in T_\varSigma$.

Proof

The proofs for the finite and the infinite cases are similar, so only the infinite case is considered. Approximately, the strategy expression $\beta$ will be the translation of the $\omega$-regular expression for the language L. Since L is $\omega$-regular, there must be a Büchi automaton $A = (Q, S, \delta , Q_0, F)$ for L. However, the symbols of the alphabet are states and our language is based on rules, so we have to translate it. The translation $B = (S \times Q, RA, \varDelta , B_0, S \times F)$ is defined using the strategies of Lemma 2, $RA = \{ \alpha _{t,t'} \mid t, t' \in S \}$ with $\varDelta ((t, q), \alpha ) = \{\; (t', q') \mid t \,\hbox {@}\,\alpha \rightarrow _{s,c}^* t' \,\hbox {@}\,\varepsilon , \; q' \in \delta (q, t') \;\}$ and $B_0 = \{\; (w_0, q) \mid w \in L, \; q \in \delta (q_0, t), \; q_0 \in Q_0 \;\}$. It is easy to prove that $\alpha _{t, t'}$ satisfies the definition of $\varDelta$ for any pair of terms and that $L = \{ v \in T_\varSigma ^\omega \mid v_k \,\hbox {@}\,w_k \rightarrow _{s,c}^* v_{k+1} \,\hbox {@}\,\varepsilon \text { for all } k \in {\mathbb {N}}, w \in L(B)\}$.

Since L(B) is $\omega$-regular, it can be expressed as an $\omega$-regular expression (Löding and Tollkötter 2016), which always have the form $r_1 s_1^\omega + \ldots r_n s_n^\omega$ for $r_i, s_i$ regular expressions and $\varepsilon \not \in L(s_i)$. The conversion from regular expressions to strategy expressions is almost an identity. $\emptyset$ is translated as ${ \texttt {fail}}$, $\varepsilon$ as ${ \texttt {idle}}$, alternation, concatenation, and iterations are the same in both languages. For each $s_i$, to represent $s_i^\omega$, we define a named strategy with label $f_i$ without argument and defined as $T(s_i) { \texttt {;}}f_i$ if T is the translation function.

Inductively, we will prove that any successful execution $t \,\hbox {@}\,T(r)$ for any regular or $\omega$-regular expression r sequentially executes all strategies in a word $w \in L(r)$, and that all words in L(r) can be successfully executed for some initial term. This implies, from what we have proved above, that the traces for T(r) are exactly L as we want to prove. Splitting the execution in RA atoms is always possible, since they are the only rule applications in the sequence enclosed by matchrew opening and closing transitions, with possibly some control steps between these atoms. The proof is by induction on the structure of regular and $\omega$-regular expressions. However, we should take care that the semantics of the iteration is different from that of the Kleene star, since the iteration body could be repeated indefinitely. Since $E(\alpha , t)$ is closed, this infinite execution will be already included, so it makes no difference.

Finally, and since the strategy satisfies the conditions of the second statement of Proposition 6, the reachable states are finite. $\square$

Proposition 6

The reachable states from $t \,\hbox {@}\,\alpha$ are finitely many if any of the following conditions holds:

• 1. $\alpha$ does not contain iterations or recursive calls.

• 2. The reachable terms from $t \,\hbox {@}\,\alpha$ are finitely many and all recursive calls in $\alpha$ and the reachable strategy definitions are tail.

Proof

The first statement can be proved by induction on the execution states ranked by the lexicographic combination of the number of strategy constructors in their stacks, the number of execution state constructors, and the number of condition fragments in $\mathrm {rewc}$ states. Looking at the rules, each possible execution state has a finite number of successors by the $\rightarrow _{s,c}$ relation, and the induction hypothesis can be applied for all but iterations and calls. In case no recursive strategies are called, reachable states can be proved finite by induction on the finite and acyclic static call graph.

For the second statement, we know that the number of terms that can appear either as subject or as strategy call arguments in execution states is finite, so iteration and tail-recursive calls can be handled. The body $\alpha$ of an iteration $\alpha \texttt {*}$ cannot contain recursive strategy calls, because it would not be tail calls. Inductively on the number of nested iterations, there are finitely many reachable states from $t \,\hbox {@}\,\alpha \texttt {*} \, s$ in addition to those from the reachable $t' \,\hbox {@}\,s$ states at the end of the iteration. Assuming there are no iterations in $\alpha$, the only successors of that state are $t \,\hbox {@}\,\alpha \, \alpha \texttt {*} \, s$ and $t \,\hbox {@}\,s$. The reachable states from $t \,\hbox {@}\,\alpha \, \alpha \texttt {*} \, s$ are those reachable from $t \,\hbox {@}\,\alpha \, \mathrm {vctx}(s)$ with $\mathrm {vctx}(s)$ replaced by $\alpha \texttt {*} \, s$, and those reachable from $t' \,\hbox {@}\,\alpha \texttt {*} \, s$ for each solution yield by $t \,\hbox {@}\,\alpha \, \mathrm {vctx}(s)$. The first are finitely many by the first statement, and the second case is the same we are proving now regardless of the particular t or $t'$, which are finitely many. Hence, the reachable states before s are finitely many, and the same can be proven if $\alpha$ contains iterations by continuing the induction.

Consider now an execution state $t \,\hbox {@}\,\textit{sl}\,(t_1, \ldots , t_n) \, \sigma \, s$ where $\textit{sl}$ is a recursive strategy. Its successors are $t \,\hbox {@}\,\delta \, \sigma ' \, s$ for some definition $\delta$ and substitution $\sigma '$. If the expression $\delta$ does not contain recursive strategies, finitely many states are reachable from $t \,\hbox {@}\,\delta \, \sigma '$. Otherwise, all recursive calls are tail and this yields finitely many states plus some $t_k \,\hbox {@}\,\textit{sl}_k(t_{k,1}, \ldots , t_{k,n_k}) \, \sigma ' \, s$ and their successors. More precisely, it should be proved that our syntactical definition of tail call ensures this, but it is a straightforward inductive check. Since the possible $t_k$, $t_{k, l}$, and $\textit{sl}_k$ are finitely many, the successors of initial state before reducing s are finitely many, and combining all the results the whole reachable states are a finite set. $\square$