A Constructor-Based Reachability Logic for Rewrite Theories

Abstract

Reachability logic has been applied to $\mathbb {K}$ rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Constructor-based semantic unification, matching, and satisfiability procedures greatly increase the range of decidable background theories that can be used in reachability logic proofs. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.

1 Introduction

The main applications of reachability logic to date have been as a language-generic logic of programs [14, 15]. In these applications, a $\mathbb {K}$ specification of a language’s operational semantics by means of rewrite rules is assumed as the language’s “golden semantic standard,” and a correct-by-construction reachability logic for a language so defined is automatically obtained [15]. This method has been effective in proving reachability properties for a wide range of programs.

Although the foundations of reachability logic are very general [14, 15], the existing theory does not provide straightforward answers to the following questions: (1) Could a reachability logic be developed to verify not just conventional programs, but also distributed system designs and algorithms formalized as rewrite theories in rewriting logic [8]? (2) If so, what would be the most natural way to conceive such a rewrite-theory-generic logic? A satisfactory answer to questions (1)–(2) would move the verification game from the level of verifying code to that of verifying both code and distributed system designs. Since the cost of design errors can be several orders of magnitude higher than that of coding errors, answering questions (1) and (2) is of practical software engineering interest.

Although a first step towards a reachability logic for rewrite theories has been taken in [6], as explained in Sect. 7 and below, that first step still leaves several important questions open. The most burning one is how to prove invariants. Since they are the most basic safety properties, support for proving invariants is a sine qua non requirement. As explained below, a serious obstacle is what we call the invariant paradox: we cannot verify in this manner any invariants of a never-terminating system such as, for example, a mutual exclusion protocol.

A second open question is how to best take advantage of the wealth of equational reasoning techniques such as matching, unification, and narrowing modulo an equational theory $(\varSigma ,E)$, and of recent results on decidable satisfiability of quantifier-free formulas in initial algebras, e.g., [9] to automate as much as possible reachability logic deduction. In this regard, the very general foundations of reachability logic—which assume any $\varSigma$-algebra $\mathcal {A}$ with a first-order-definable transition relation—provide no help at all for automation. As shown in this work and its prototype implementation, if we assume instead that the model in question is the initial model $\mathcal {T}_{\mathcal {R}}$ of a rewrite theory $\mathcal {R}$ satisfying reasonable assumptions, large parts of the verification effort can be automated.

A third important issue is simplicity. Reachability logic has eight inference rules [14, 15]. Could a reachability logic for rewrite theories be simpler? This work tackles head on these three open questions to provide a general reachability logic and a prototype implementation suitable for reasoning about properties of both distributed systems and programs based on their rewriting logic semantics.

Rewriting Logic in a Nutshell. A distributed system can be designed and modeled as a rewrite theory $\mathcal {R}=(\varSigma ,E,R)$ [8] in the following way: (i) the distributed system’s states are modeled as elements of the initial algebra $T_{\varSigma /E}$ associated to the equational theory $(\varSigma ,E)$ with function symbols $\varSigma$ and equations E; and (ii) the system’s concurrent transitions are modeled by rewrite rules R, which are applied modulo E. Let us consider the QLOCK [5] mutual exclusion protocol, explained in detail in Sect. 2. QLOCK allows an unbounded number of processes, which can be identified by numbers. Such processes can be in one of three states: “normal” (doing their own thing), “waiting” for a resource, and “critical,” i.e., using the resource. Waiting processes enqueue their identifier at the end of a waiting queue and can become critical when their name appears at the head of the queue. A QLOCK state can be represented as a tuple $<n\ |\ w\ |\ c\ |\ q>$ where n, resp. w, resp. c, denotes the set of identifiers for normal, resp. waiting, resp. critical processes, and q is the waiting queue. QLOCK can be modeled as a rewrite theory $\mathcal {R}=(\varSigma ,E,R)$, where E includes axioms such as associativity-commutativity of multiset union, list associativity, and identity axioms for $\emptyset$ and $nil$. QLOCK’s behavior is specified by five rewrite rules R. Rule $w2c$ below specifies a waiting process i becoming critical

$$ w2c :<n\ |\ w\, i\ |\ c\ |\ i;q> \rightarrow <n\ |\ w\ |\ c\,i \ |\ i;q>. $$

Reachability Logic in a Nutshell. A reachability logic formula has the form $A \rightarrow ^{\circledast } B$, with A and B state predicates (see Sect. 3). Assume for simplicity that $vars (A) \cap vars (B) = \emptyset$. Such a formula is then interpreted in the initial model $\mathcal {T}_{\mathcal {R}}$ of a rewrite theory $\mathcal {R}=(\varSigma ,E,R)$, whose states are E-equivalence classes [u] of ground $\varSigma$-terms, and where a state transition $[u] \rightarrow _{\mathcal {R}} [v]$ holds iff $\mathcal {R} \vdash u \rightarrow v$ according to the rewriting logic inference system [8] (computation = deduction). As a first approximation, $A \rightarrow ^{\circledast } B$ is a Hoare logic partial correctness assertion of the form $\{A\} \mathcal {R} \{B\}$, but with the slight twist that B need not hold of a terminating state, but just somewhere along the way. To be fully precise, $A \rightarrow ^{\circledast } B$ holds in $\mathcal {T}_{\mathcal {R}}$ iff for each state $[u_{0}]$ satisfying A and each terminating sequence $[u_{0}] \rightarrow _{\mathcal {R}} [u_{1}] \ldots \rightarrow _{\mathcal {R}} [u_{n-1}] \rightarrow _{\mathcal {R}} [u_{n}]$ there is a j, $0 \le j \le n$ such that $[u_{j}]$ satisfies B. A key question is how to choose a good language of state predicates like A and B. Here is where the potential for increasing the logic’s automation resides. We call our proposed logic constructor-based, because our choice is to make A and B positive (only $\vee$ and $\wedge$) combinations of what we call constructor patterns of the form $u \mid \varphi$, where u is a constructor term¹ and $\varphi$ a quantifier-free (QF) $\varSigma$-formula. The state predicate $u \mid \varphi$ holds for a state $[u']$ iff there is a ground substitution $\rho$ such that $[u']=[u \rho ]$ and $E \models \varphi \rho$.

The Invariant Paradox. How can we prove invariants in such a reachability logic? For example, mutual exclusion for QLOCK? Paradoxically, we cannot! This is because QLOCK, like many other protocols, never terminates, that is, has no terminating sequences whatsoever. And this has the ludicrous trivial consequence that QLOCK’s initial model $\mathcal {T}_{\mathcal {R}}$ vacuously satisfies all reachability formulas $A \rightarrow ^{\circledast } B$. This of course means that it is in fact impossible to prove any invariants using reachability logic in the initial model $\mathcal {T}_{\mathcal {R}}$. But it does not mean that it is impossible using some other initial model. In Sect. 4.1 we give a systematic solution to this paradox by means of a simple theory transformation allowing us to prove any invariant in the original initial model $\mathcal {T}_{\mathcal {R}}$ by proving an equivalent reachability formula in the initial model of the transformed theory.

Our Contributions. Section 2 gathers preliminaries. The main theoretical contributions of a simple semantics and inference system for a rewrite-theory-generic reachability logic with just two inference rules and its soundness are developed in Sects. 4 and 5. A systematic methodology to prove invariants by means of reachability formulas is developed in Sect. 4.1. The goal of increasing the logic’s potential for automation by making it constructor-based is advanced in Sects. 3–5. A proof of concept of the entire approach is given by means of a Maude-based prototype implementation and a suite of experiments verifying various properties of distributed system designs in Sect. 6. Related work and conclusions are discussed in Sect. 7. Proofs can be found in [13].

2 Many-Sorted Algebra and Rewriting Logic

We present some preliminaries on many-sorted algebra and rewriting logic. For a more general treatment using order-sorted algebra see [13]. Readers familiar with many-sorted logic may go directly to Definition 1. We assume familiarity with the following basic concepts and notation that are explained in full detail in, e.g., [10]: (i) many-sorted (MS) signature as a pair $\varSigma = (S,\varSigma )$ with S a set of sorts and $\varSigma$ an $S^{*} \times S$-indexed family $\varSigma = \{\varSigma _{w,s}\}_{(w,s) \in S^{*} \times S}$ of function symbols, where $f \in \varSigma _{s_{1} \ldots s_{n},s}$ is displayed as $f: s_{1} \ldots s_{n} \rightarrow s$; (ii) $\varSigma$ -algebra A as a pair $A =(A,\_{_{A}})$ with $A=\{A_{s}\}_{s \in S}$ an S-indexed family of sets, and $\_{_{A}}$ a mapping interpreting each $f: s_{1} \ldots s_{n} \rightarrow s$ as a function in the set $[A_{s_{1}} \times \ldots \times A_{s_{n}}\rightarrow A_s]$. (iii) $\varSigma$-homomorphism $h: A \rightarrow B$ as an S-indexed family of functions $h =\{h_{s}: A_{s} \rightarrow B_{s}\}_{s \in S}$ preserving the operations in $\varSigma$; (iv) the term $\varSigma$-algebra $T_{\varSigma }$ and its initiality in the category $\mathbf{MSAlg}_{\varSigma }$ of $\varSigma$-algebras when $\varSigma$ is unambiguous.

An S-sorted set $X=\{X_{s}\}_{s \in S}$ of variables, satisfies $s \not = s' \Rightarrow X_{s}\cap X_{s'}=\emptyset$, and the variables in X are always assumed disjoint from all constants in $\varSigma$. The $\varSigma$-term algebra on variables X, $T_{\varSigma }(X)$, is the initial algebra for the signature $\varSigma (X)$ obtained by adding to $\varSigma$ the variables X as extra constants. Since a $\varSigma (X)$-algebra is just a pair $(A,\alpha )$, with A a $\varSigma$-algebra, and $\alpha$ an interpretation of the constants in X, i.e., an S-sorted function $\alpha \in [X {{\small \rightarrow }}A]$, the $\varSigma (X)$-initiality of $T_{\varSigma }(X)$ means that for each $A \in \mathbf{MSAlg}_{\varSigma }$ and $\alpha \in [X {{\small \rightarrow }}A]$, there exists a unique $\varSigma$-homomorphism, $\_\alpha : T_{\varSigma }(X) \rightarrow A$ extending $\alpha$, i.e., such that for each $s \in S$ and $x \in X_{s}$ we have $x \alpha _{s} = \alpha _{s}(x)$. In particular, when $A=T_{\varSigma }(Y)$, an interpretation of the constants in X, i.e., an S-sorted function $\sigma \in [X {{\small \rightarrow }}T_{\varSigma }(Y)]$ is called a substitution, and its unique homomorphic extension $\_\sigma : T_{\varSigma }(X) \rightarrow T_{\varSigma }(Y)$ is also called a substitution. Define $dom (\sigma )=\{x \in X \mid x \not = x \sigma \}$, and $ran (\sigma )= \bigcup _{x \in dom (\sigma )} vars (x \sigma )$. Given variables Z, the substitution $\sigma |_{Z}$ agrees with $\sigma$ on Z and is the identity elsewhere.

We also assume familiarity with many-sorted first-order logic including: (i) the first-order language of $\varSigma$-formulas for $\varSigma$ a signature (in our case $\varSigma$ has only function symbols and the $=$ predicate); (ii) given a $\varSigma$-algebra A, a formula $\varphi \in Form (\varSigma )$, and an assignment $\alpha \in [Y {{\small \rightarrow }}A]$, with $Y= fvars (\varphi )$ the free variables of $\varphi$, the satisfaction relation $A,\alpha \models \varphi$ (iii) the notions of a formula $\varphi \in Form (\varSigma )$ being valid, denoted $A \models \varphi$, resp. satisfiable in a $\varSigma$-algebra A. For a subsignature $\varOmega \subseteq \varSigma$ and $A \in \mathbf{MSAlg}_{\varSigma }$, the reduct $A|_{\varOmega } \in \mathbf{MSAlg}_{\varOmega }$ agrees with A in the interpretation of all sorts and operations in $\varOmega$ and discards everything in $\varSigma \setminus \varOmega$. If $\varphi \in Form (\varOmega )$ we have the equivalence $A \models \varphi \; \Leftrightarrow \; A|_{\varOmega } \models \varphi$.

An MS equational theory is a pair $T=(\varSigma ,E)$, with E a set of (possibly conditional) $\varSigma$-equations. $\mathbf{MSAlg}_{(\varSigma ,E)}$ denotes the full subcategory of $\mathbf{MSAlg}_{\varSigma }$ with objects those $A \in \mathbf{MSAlg}_{\varSigma }$ such that $A \models E$, called the $(\varSigma ,E)$-algebras. $\mathbf{MSAlg}_{(\varSigma ,E)}$ has an initial algebra $T_{\varSigma /E}$ [10]. The inference system in [10] is sound and complete for MS equational deduction, i.e., for any MS equational theory $(\varSigma ,E)$, and $\varSigma$-equation $u=v$ we have an equivalence $E \vdash u=v \; \Leftrightarrow \; E \models u=v$. For the sake of simpler inference we assume non-empty sorts, i.e., $\forall s \in S\; T_{\varSigma },s \not = \emptyset$. Deducibility $E \vdash u=v$ is abbreviated as $u =_{E} v$, called E-equality. An E-unifier of a system of $\varSigma$-equations, i.e., a conjunction $\phi =u_{1}=v_{1} \, \wedge \, \ldots \, \wedge \, u_{n}=v_{n}$ of $\varSigma$-equations is a substitution $\sigma$ such that $u_{i} \sigma =_{E} v_{i}\sigma$, $1 \le i \le n$. An E-unification algorithm for $(\varSigma ,E)$ is an algorithm generating a complete set of E-unifiers $Unif _{E}(\phi )$ for any system of $\varSigma$ equations $\phi$, where “complete” means that for any E-unifier $\sigma$ of $\phi$ there is a $\tau \in Unif _{E}(\phi )$ and a substitution $\rho$ such that $\sigma =_{E} (\tau \rho )|_{ dom (\sigma ) \cup dom (\tau )}$, where $=_{E}$ here means that for any variable x we have $x\sigma =_{E} x (\tau \rho )|_{ dom (\sigma ) \cup dom (\tau )}$. The algorithm is finitary if it always terminates with a finite set $Unif _{E}(\phi )$ for any $\phi$.

We recall some basic concepts about rewriting logic. The survey in [8] gives a fuller account. A rewrite theory $\mathcal {R}$ axiomatizes a distributed system, so that concurrent computation is modeled as concurrent rewriting with the rules of $\mathcal {R}$ modulo the equations of $\mathcal {R}$. Recall also the following notation from [3]: (i) positions in a term viewed as a tree are marked by strings $p \in \mathbb {N}^{*}$ specifying a path from the root, (ii) $t|_{p}$ denotes the subterm of term t at position p, and (iii) $t[u]_{p}$ denotes the result of replacing subterm $t|_{p}$ at position p by u.

Definition 1

A rewrite theory is a 3-tuple $\mathcal {R}=(\varSigma ,E \cup B,R)$ with $(\varSigma ,E \cup B)$ an MS equational theory and R a set of conditional $\varSigma$-rewrite rules $l \rightarrow r \; if \; \phi$, with $l,r \in T_{\varSigma }(X)_{s}$ for some $s \in S$, and $\phi$ a quantifier-free $\varSigma$-formula. We further assume that: (1) Each equation $u=v \in B$ is regular, i.e., $vars (u) = vars (v)$, and linear, i.e., there are no repeated variables in either u or v. (2) The equations E, when oriented as conditional rewrite rules $\vec {E}=\{u \rightarrow v \; if \; \psi \mid u=v \; if \; \psi \in E\}$, are convergent modulo B, i.e., strictly coherent, confluent, and operationally terminating as rewrite rules modulo B [7]. (3) The rules R are ground coherent with the equations E modulo B [4].

Conditions (1)–(2) ensure that the initial algebra $T_{\varSigma /E \cup B}$ is isomorphic to the canonical term algebra $C_{\varSigma /E,B}$, whose elements are B-equivalence classes of $\vec {E},B$-irreducible ground $\varSigma$-terms. Define the one-step R, B-rewrite relation $t \rightarrow _{R,B} t'$ between ground terms as follows. For $t,t'\in T_{\varSigma ,s}$, $s\in S$, $t \rightarrow _{R,B} t'$ holds iff there is a rewrite rule $l\rightarrow r \; if \; \phi \in R$, a ground substitution $\sigma \in [Y {{\small \rightarrow }}T_{\varSigma }]$ with Y the rule’s variables, and a term position p in t such that $t|_{p}=_{B} l \sigma$, $t'=t[r \sigma ]_{p}$, and $E \cup B \models \phi \sigma$. In the context of (1)–(2), condition (3) ensures that “computing $\vec {E},B$-canonical forms before performing R, B-rewriting” is a complete strategy. That is, if $t \rightarrow _{R,B} t'$ and $u = t!_{E,B}$, i.e., $t \rightarrow ^{*}_{\vec {E},B} u$ with u in $\vec {E},B$-canonical form (abbreviated in what follows to $u = t!$), then there exists a $u'$ such that $u \rightarrow _{R,B} u'$ and $t'! =_{B} u'!$. Note that $vars (r) \subseteq vars (l)$ is nowhere assumed for rules $l\rightarrow r \; if \; \phi \in R$. This means that $\mathcal {R}$ can specify an open system, in the sense of [11], that interacts with an external, non-deterministic environment such as, for example, a thermostat.

Conditions (1)–(3) allow a simple description of the initial reachability model $\mathcal {T}_{\mathcal {R}}$ [8] of $\mathcal {R}$ as the canonical reachability model $\mathcal {C}_{\mathcal {R}}$ whose states belong to the canonical term algebra $C_{\varSigma /E,B}$, and the one-step transition relation $[u] \rightarrow _{\mathcal {R}} [v]$ holds iff $u \rightarrow _{R,B} u'$ and $[u'!] = [v]$. Furthermore, if $u \rightarrow _{R,B} u'$ has been performed with a rewrite rule $l\rightarrow r \; if \; \phi \in R$ and a ground substitution $\sigma \in [Y {{\small \rightarrow }}T_{\varSigma }]$, then, assuming B-equality is decidable, checking whether condition $E \cup B \models \phi \sigma$ holds is decidable by reducing the terms in $\phi \sigma$ to $\vec {E},B$-canonical form.

A Running Example. Consider the following rewrite theory $\mathcal {R}=(\varSigma ,E \cup B,R)$ modeling a dynamic version of the QLOCK mutual exclusion protocol [5], where $(\varSigma ,B)$ defines the protocol’s states, involving natural numbers, lists, and multisets over natural numbers. $\varSigma$ has sorts $S=\{ Nat , List , MSet , Conf , State , Pred \}$ with subsorts² $Nat < List$ and $Nat < MSet$ and operators $F=\{ 0 :\ \rightarrow Nat ,\ s\_ : Nat \rightarrow Nat ,\ \emptyset :\ \rightarrow MSet ,\ nil :\ \rightarrow List ,$ $\_\_ : MSet\ MSet \rightarrow MSet ,\ \_;\_ : List\ List \rightarrow List , dupl : MSet \rightarrow Pred , tt :\ \rightarrow Pred , <\_> : Conf \rightarrow State , \_|\_|\_|\_ : MSet\ MSet\ MSet\ List \rightarrow Conf \}$, where underscores denote operator argument placement. The axioms B are the associativity-commutativity of the multiset union $\_\_$ with identity $\emptyset$, and the associativity of list concatenation $\_;\_$ with identity $nil$. The only equation in E is $dupl(s\, i \, i) = tt$. It defines the $dupl$ predicate by detecting a duplicated element i in the multiset $s\, i \, i$ (s could be empty). States of QLOCK are B-equivalence classes of ground terms of sort $State$.

QLOCK [5] is a mutual exclusion protocol where the number of processes is unbounded. Furthermore, in the dynamic version of QLOCK presented below, such a number can grow or shrink. Each process is identified by a number. The system configuration has three sets of processes (normal, waiting, and critical) plus a waiting queue. To ensure mutual exclusion, a normal process must first register its name at the end of the waiting queue. When its name appears at the front of the queue, it is allowed to enter the critical section. The first three rewrite rules in R below specify how a normal process i first transitions to a waiting process, then to a critical process, and back to normal. The last two rules in R specify how a process can dynamically join or exit the system.

where $\phi \equiv dupl (n \, i \, w\ c)\ne tt$, $i$ is a number, $n$, $w$, and $c$ are, respectively, normal, waiting, and critical process identifier sets, and $q$ is a queue of process identifiers. It is easy to check that $\mathcal {R}=(\varSigma ,E \cup B,R)$ satisfies requirements (1)–(3). Note that $join$ makes QLOCK an open system in the sense explained above.

3 Constrained Constructor Pattern Predicates

Given an MS equational theory $(\varSigma ,E \cup B)$, the atomic state predicates appearing in the constructor-based reachability logic formulas of Sect. 4 will be pairs $u \mid \varphi$, called constrained constructor patterns, with u a term in a subsignature $\varOmega \subseteq \varSigma$ of constructors, and $\varphi$ a quantifier-free $\varSigma$-formula. Intuitively, $u \mid \varphi$ is a pattern describing the set of states that are $E_{\varOmega } \cup B_{\varOmega }$-equal to ground terms of the form $u \rho$ for $\rho$ a ground constructor substitution such that $E \cup B \models \varphi \rho$. Therefore, $u \mid \varphi$ can be used as a symbolic description of a, typically infinite, set of states in the canonical reachability model $\mathcal {C}_{\mathcal {R}}$ of a rewrite theory $\mathcal {R}$.

Often, the signature $\varSigma$ on which $T_{\varSigma /E \cup B}$ is defined has a natural decomposition as a disjoint union $\varSigma = \varOmega \uplus \varDelta$, where the elements of the canonical term algebra $C_{\varSigma /E,B}$ are $\varOmega$-terms, whereas the function symbols $f \in \varDelta$ are viewed as defined functions which are evaluated away by $\vec {E},B$-simplification. $\varOmega$ (with same poset of sorts as $\varSigma$) is then called a constructor subsignature of $\varSigma$.

A decomposition of a MS equational theory $(\varSigma ,E \cup B)$ is a triple $(\varSigma ,B,\vec {E})$ such that the rules $\vec {E}$ are convergent modulo B. $(\varSigma ,B,\vec {E})$ is called sufficiently complete with respect to the constructor subsignature $\varOmega$ iff for each $t \in T_{\varSigma }$ we have: (i) $t!_{\vec {E},B} \in T_{\varOmega }$, and (ii) if $u \in T_{\varOmega }$ and $u =_{B} v$, then $v \in T_{\varOmega }$. This ensures that for each $[u]_{B} \in C_{\varSigma /E,B}$ we have $[u]_{B} \subseteq T_{\varOmega }$. Sufficient completeness is closely related to the notion of a protecting inclusion of decompositions.

Definition 2

Let $(\varSigma _{0},E_{0} \cup B_{0}) \subseteq (\varSigma ,E \cup B)$ be a theory inclusion such that $(\varSigma _{0},B_{0},\vec {E_{0}})$ and $(\varSigma ,B,\vec {E})$ are respective decompositions of $(\varSigma _{0},E_{0} \cup B_{0})$ and $(\varSigma ,E \cup B)$. We then say that the decomposition $(\varSigma ,B,\vec {E})$ protects $(\varSigma _{0},B_{0},\vec {E_{0}})$ iff (i) for all $t,t' \in T_{\varSigma _{0}}(X)$ we have: (i) $t=_{B_0} t' \Leftrightarrow t=_{B} t'$, (ii) $t=t!_{\vec {E_0},B_{0}} \Leftrightarrow t=t!_{\vec {E},B}$, and (iii) $C_{\varSigma _{0}/E_{0},B_{0}}=C_{\varSigma /E,B}|_{\varSigma _{0}}$.

$(\varOmega ,B_{\varOmega },\vec {E_{\varOmega }})$ is a constructor decomposition of $(\varSigma ,B,\vec {E})$ iff (i) $(\varSigma ,B,\vec {E})$ protects $(\varOmega ,B_{\varOmega },\vec {E_{\varOmega }})$, and (ii) $(\varSigma ,B,\vec {E})$ is sufficiently complete with respect to the constructor subsignature $\varOmega$. Furthermore, $\varOmega$ is called a subsignature of free constructors modulo $B_{\varOmega }$ iff $E_{\varOmega } = \emptyset$, so that $C_{\varOmega /E_{\varOmega },B_{\varOmega }}=T_{\varOmega /B_{\varOmega }}$.

We are now ready to define constrained constructor pattern predicates.

Definition 3

Let $(\varOmega ,B_{\varOmega },\vec {E_{\varOmega }})$ be a constructor decomposition of $(\varSigma ,B,\vec {E})$. A constrained constructor pattern is an expression $u \mid \varphi$ with $u \in T_{\varOmega }(X)$ and $\varphi$ a QF $\varSigma$-formula. The set $PatPred (\varOmega ,\varSigma )$ of constrained constructor pattern predicates contains $\bot$ and the set of constrained constructor patterns, and is closed under disjunction ($\vee \!$) and conjunction ($\wedge \!$). Capital letters $A,B,\ldots ,P,Q,\ldots$ range over $PatPred (\varOmega ,\varSigma )$. The semantics of a constrained constructor pattern predicate A is a subset $\llbracket A \rrbracket \subseteq C_{\varSigma /E,B}$ defined inductively as follows:

• 1. $\llbracket \bot \rrbracket = \emptyset$

• 2. $\llbracket u \mid \varphi \rrbracket = \{[(u \rho )!]_{B_{\varOmega }} \in C_{\varSigma /E,B} \mid \rho \in [X {{\small \rightarrow }}T_{\varOmega }] \, \wedge \, E \cup B \models \varphi \rho \}$.

• 3. $\llbracket A \vee B \rrbracket$ = $\llbracket A \rrbracket \cup \llbracket B \rrbracket$

• 4. $\llbracket A \wedge B \rrbracket$ = $\llbracket A \rrbracket \cap \llbracket B \rrbracket$.

Note that for any constructor pattern predicate A, if $\sigma$ is a (sort-preserving) bijective renaming of variables we always have $\llbracket A \rrbracket = \llbracket A \sigma \rrbracket$. Given constructor patterns $u \mid \varphi$ and $v \mid \psi$ with $vars (u \mid \varphi ) \cap vars (v \mid \psi ) = \emptyset$, we say that $u \mid \varphi$ subsumes $v \mid \psi$ iff there is a substitution $\alpha$ such that: (i) $v =_{E_{\varOmega } \cup B_{\varOmega }} u \alpha$, and (ii) $\mathcal {T}_{E \cup B} \models \psi \Rightarrow (\varphi \alpha )$. It then follows easily from the above definition of $\llbracket u \mid \varphi \rrbracket$ that if $u \mid \varphi$ subsumes $v \mid \psi$, then $\llbracket v \mid \psi \rrbracket \subseteq \llbracket u \mid \varphi \rrbracket$. Likewise, $\bigvee _{i \in I} u_i \mid \varphi _i$ subsumes $v \mid \psi$ iff there is a $k \in I$ such that $u_k \mid \varphi _k$ subsumes $v \mid \psi$.

Pattern Predicate Example. Letting $n$, $w$, $c$ be multisets of process identifiers and $q$ be an associative list of process identifiers, recall that QLOCK states have the form $<n\ |\ w\ |\ c\ |\ q>$. From the five rewrite rules defining QLOCK, it is easy to prove that if $<n\ |\ w\ |\ c\ |\ q> \rightarrow ^* <n'\ |\ w'\ |\ c'\ |\ q'>$ and $n \, w \, c$ is a set (has no repeated elements), then $n' \, w' \, c'$ is also a set. Of course, it seems very reasonable to assume that these process identifier multisets are, in fact, sets, since otherwise we could, for example, have a process i which is both waiting and critical at the same time. We can rule out such ambiguous states by means of the pattern predicate $<n\ |\ w\ |\ c\ |\ q> \ |\ dupl ( n\ w\ c )\ne tt$.

If $E_{\varOmega } \cup B_{\varOmega }$ has a finitary unification algorithm, any constrained constructor pattern predicate A is semantically equivalent to a finite disjunction $\bigvee _{i} u_{i} \mid \varphi _{i}$ of constrained constructor patterns. This is because: (i) by (3)–(4) in Definition 3 we may assume A in disjunctive normal form; and (ii) it is easy to check that $\llbracket (u \mid \varphi ) \wedge (v \mid \phi ) \rrbracket$ = $\bigcup _{\alpha \in Unif _{E_{\varOmega } \cup B_{\varOmega }}(u,v)} \llbracket u \alpha \mid (\varphi \wedge \phi ) \alpha \rrbracket$, were we assume that $vars (u \mid \varphi ) \cap vars (v \mid \psi ) = \emptyset$, and that all variables in $ran (\alpha )$ are fresh. Pattern intersection can also be defined when $u \mid \varphi$ and $v \mid \phi$ share parameters $Y= vars (u \mid \varphi ) \cap vars (v \mid \phi ) = vars (u) \cap vars (v)$. [13] defines in detail the notions of parametric intersection $\llbracket u \mid \varphi \rrbracket \cap _{Y} \llbracket v \mid \phi \rrbracket$ and of parametric subsumption $v \mid \phi \subseteq _{Y} u \mid \varphi$ of patterns. These notions are very useful to reason about parameterized invariants and co-invariants (see Sect. 4.1 and [13]).

4 Constructor-Based Reachability Logic

The constructor-based reachability logic we define is a logic to reason about reachability properties of the canonical reachability model $\mathcal {C}_{\mathcal {R}}$ of a topmost rewrite theory $\mathcal {R}$ where “topmost” intuitively means all rewrites must occur at the top of the term.³ Many rewrite theories of interest, including those specifying distributed object-oriented systems or the semantics of (possibly concurrent) programming languages, can be easily made topmost by a theory transformation (see, e.g., [16]). Formally, we require $\mathcal {R}=(\varSigma ,E \cup B,R)$, besides satisfying the requirements in Definition 1, also satisfies:

• 1. $(\varSigma ,E \cup B)$ has a sort $State$, a decomposition $(\varSigma ,B,\vec {E})$, and a constructor decomposition $(\varOmega ,B_{\varOmega },\vec {E_{\varOmega }})$ where: (i) $\forall u \in T_{\varOmega }(X)_{ State }$, $vars (u)= vars (u!)$; (ii) $B_{\varOmega }$ are linear and regular with a finitary $E_{\varOmega } \cup B_{\varOmega }$-unification algorithm.

• 2. Rules in R have the form $l\rightarrow r \; if \; \varphi$ with $l \in T_{\varOmega }(X)$. Furthermore, they are topmost in the sense that: (i) for all such rules, l and r have sort $State$, and (ii) for any $u \in T_{\varOmega }(X)_{ State }$ and any non-empty position p in u, $u|_{p} \not \in T_{\varOmega }(X)_{ State }$.

Requirements (1)–(2) ensure that in the canonical reachability model $\mathcal {C}_{\mathcal {R}}$ if $[u] \rightarrow _{\mathcal {R}} [v]$ holds, then the R, B-rewrite $u \rightarrow _{R,B} u'$ such that $[u'!] = [v]$ happens at the top of u, i.e., uses a rewrite rule $l\rightarrow r \; if \; \varphi \in R$ and a ground substitution $\sigma \in [Y {{\small \rightarrow }}T_{\varOmega }]$, with Y the rule’s variables, such that $u =_{B_{\varOmega }} l \sigma$ and $u'=r \sigma$.

We are now ready to define the formulas of our constructor-based reachability logic for $\mathcal {R}$ satisfying above requirements (1)–(2). Let $PatPred (\varOmega ,\varSigma )_{ State }$ denote the subset of $PatPred (\varOmega ,\varSigma )$ determined by those pattern predicates A such that, for all atomic constrained constructor predicates $u \mid \varphi$ appearing in A, u has sort $State$. Reachability logic formulas then have the form: $A \rightarrow ^{\circledast } B$, with $A,B \in PatPred (\varOmega ,\varSigma )_{ State }$. The parameters Y of $A \rightarrow ^{\circledast } B$ are the variables in the set $Y= vars (A) \cap vars (B)$, and $A \rightarrow ^{\circledast } B$ is called unparameterized iff $Y=\emptyset$.

The reachability logic in [14, 15] is based on terminating sequences of state transitions; when there are no terminating states, all reachability formulas are vacuously true. Our purpose is to extend the logic in order to verify properties of general distributed systems specified as rewrite theories $\mathcal {R}$ which may never terminate. For this, as explained in Sect. 4.1, we generalize the all-paths satisfaction relation in [15], which for a theory $\mathcal {R}$ we denote by $\mathcal {R} \models ^{\forall } A \rightarrow ^{\circledast } B$, to a relativized satisfaction relation $\mathcal {R} \models _{T}^{\forall } A \rightarrow ^{\circledast } B$, where T is a constrained pattern predicate such that $\llbracket T \rrbracket$ is a set of terminating states. That is, let $Term _{\mathcal {R}} = \{ [u] \in \mathcal {C}_{\mathcal {R}, State } \mid (\not \exists [v])\; [u] \rightarrow _{\mathcal {R}} [v]\}$. We then require $\llbracket T \rrbracket \subseteq Term _{\mathcal {R}}$. The standard relation $\mathcal {R} \models ^{\forall } A \rightarrow ^{\circledast } B$ is then recovered as the special case where $\llbracket T \rrbracket = Term _{\mathcal {R}}$. Call $[u] \rightarrow ^{*}_{\mathcal {R}}[v]$ a T-terminating sequence iff $[v] \in \llbracket T \rrbracket$.

Definition 4

Given T with $\llbracket T \rrbracket \subseteq Term _{\mathcal {R}}$, the all-paths satisfaction relation $\mathcal {R} \models _{T}^{\forall } u \mid \varphi \rightarrow ^{\circledast } \bigvee _{j \in J} v_{j} \mid \phi _{j}$ asserts the satisfaction of the formula $u \mid \varphi \rightarrow ^{\circledast } \bigvee _{j \in J} v_{j} \mid \phi _{j}$ in the canonical reachability model $\mathcal {C}_{\mathcal {R}}$ of a rewrite theory $\mathcal {R}$ satisfying topmost requirements (1)–(2). It is defined as follows:

For $u \mid \varphi \rightarrow ^{\circledast } \bigvee _{j \in J} v_{j} \mid \phi _{j}$ unparameterized, $\mathcal {R} \models _{T}^{\forall } u \mid \varphi \rightarrow ^{\circledast } \bigvee _{j \in J} v_{j} \mid \phi _{j}$ holds iff for each T-terminating sequence $[u_{0}] \rightarrow _{\mathcal {R}}[u_{1}] \ldots [u_{n-1}]\rightarrow _{\mathcal {R}}[u_{n}]$ with $[u_{0}] \in \llbracket u \mid \varphi \rrbracket$ there exist k, $0 \le k \le n$ and $j \in J$ such that $[u_{k}] \in \llbracket v_{j} \mid \phi _{j} \rrbracket$. For $u \mid \varphi \rightarrow ^{\circledast } \bigvee _{j \in J} v_{j} \mid \phi _{j}$ with parameters Y, $\mathcal {R} \models _{T}^{\forall } u \mid \varphi \rightarrow ^{\circledast } \bigvee _{j \in J} v_{j} \mid \phi _{j}$ holds if $\mathcal {R} \models _{T}^{\forall } (u \mid \varphi )\rho \rightarrow ^{\circledast } (\bigvee _{j \in J} v_{j} \mid \phi _{j})\rho$ holds for each $\rho \in [Y {{\small \rightarrow }}T_{\varOmega }]$.

Since a constrained pattern predicate is equivalent to a disjunction of atomic ones, we can define satisfaction on general reachability logic formulas as follows: $\mathcal {R} \models _{T}^{\forall } \bigvee _{1 \le i \le n} u_i \mid \varphi _i \rightarrow ^{\circledast } A$ iff $\bigwedge _{1 \le i \le n} \mathcal {R} \models _{T}^{\forall } u_i \mid \varphi _i \rightarrow ^{\circledast } A$, assuming same parameters $Y_{i}= vars (u_i \mid \varphi _i) \cap vars (A)$, i.e., $Y_{i}=Y_{i'}$ for $1 \le i < i' \le n$.

$\mathcal {R} \models _{T}^{\forall } A \rightarrow ^{\circledast } B$ is a partial correctness assertion: If state [u] satisfies “precondition” A, then “postcondition” B is satisfied somewhere along each T-terminating sequences from [u], generalizing a Hoare formula $\{A\} \mathcal {R} \{B\}$ [13].

Recall that rewrite rules $l\rightarrow r \; if \; \phi$ are assumed to have $l \in T_{\varOmega }(X)$. For symbolic reasoning purposes it will be very useful to also require that $r \in T_{\varOmega }(X)$. This can be achieved by a theory transformation $\mathcal {R} \mapsto \hat{\mathcal {R}}$. Stated formally, if $\mathcal {R}=(\varSigma ,E \cup B,R)$, then $\hat{\mathcal {R}}=(\varSigma ,E \cup B,\hat{R})$, where the rules $\hat{R}$ are obtained from the rules R by transforming each $l\rightarrow r \; if \; \phi$ in R into the rule $l\rightarrow r' \; if \; \phi \wedge \hat{\theta }$, where: (i) $r'$ is the $\varOmega$-abstraction of r obtained by replacing each length-minimal position p of r such that $t|_{p} \not \in T_{\varOmega }(X)$ by a fresh variable $x_{p}$ whose sort is the least sort of $t|_{p}$, (ii) $\hat{\theta } = \bigwedge _{p\in P} x_{p} = t_{p}$, where P is the set of all length-minimal positions in r such that $t|_{p} \not \in T_{\varOmega }(X)$.

The key semantic property about this transformation is:

Lemma 1

The canonical reachability models $\mathcal {C}_{\mathcal {R}}$ and $\mathcal {C}_{\hat{\mathcal {R}}}$ are identical.

4.1 Invariants, Co-Invariants, and Never-Terminating Systems

The notion of an invariant applies to any transition system $\mathcal {S} = (S,\rightarrow _{\mathcal {S}})$ with states S and transition relation $\rightarrow _{\mathcal {S}} \subseteq S \times S$. The set $Reach (S_{0})$ of states reachable from $S_{0} \subseteq S$ is defined as $Reach (S_{0}) = \{s \in S \mid (\exists s_{0} \in S_{0})\; s_{0} \rightarrow ^{*}_{\mathcal {S}} s \}$, where $\rightarrow ^{*}_{\mathcal {S}}$ denotes the reflexive-transitive closure of $\rightarrow _{\mathcal {S}}$. An invariant about $\mathcal {S}$ with initial states $S_{0}$ can be specified in two ways: (i) by a “good” property $P \subseteq S$, the invariant, that always holds from $S_{0}$, i.e., such that $Reach (S_{0}) \subseteq P$, or (ii) as a “bad” property $Q \subseteq S$, the co-invariant, that never holds from $S_{0}$, i.e., such that $Reach (S_{0}) \cap Q = \emptyset$. Obviously, P is an invariant iff $S \setminus P$ is a co-invariant.

Suppose we have specified a distributed system by a topmost rewrite theory $\mathcal {R}$, and constrained pattern predicates $S_{0}$ and P, and we want to prove that $\llbracket P \rrbracket$ is an invariant of the system $(\mathcal {C}_{\mathcal {R}, State },\rightarrow _{\mathcal {R}})$ from $\llbracket S_{0} \rrbracket$. Can we specify such invariant or co-invariant by means of reachability formulas and use the inference system of Sect. 5 to try to prove such formulas?

The answer to the above question is not obvious. Suppose $\mathcal {R}$ specifies a never-terminating system, i.e., $Term _{\mathcal {R}}= \emptyset$. For example, QLOCK and other mutual exclusion protocols are never-terminating. Then, no reachability formula can characterize and invariant holding by means of the satisfaction relation $\mathcal {R} \models _{T}^{\forall } A \rightarrow ^{\circledast } B$. The reason for this impossibility is that, since $Term _{\mathcal {R}}= \emptyset$, $\mathcal {R} \models ^{\forall }_{T} A \rightarrow ^{\circledast } B$ holds vacuously for all reachability formulas $A \rightarrow ^{\circledast } B$.

Is then reachability logic useless to prove invariants? Definitely not. We need to first perform a simple theory transformation. Call an invariant specifiable by constrained pattern predicates $S_{0}$ and P if $\llbracket P \rrbracket$ is an invariant of $(\mathcal {C}_{\mathcal {R}, State },\rightarrow _{\mathcal {R}})$ from $\llbracket S_{0} \rrbracket$. To ease the exposition, we explain the transformation for the case where $\varOmega$ has a single state constructor operator, say, $\langle \_,\ldots ,\_\rangle : s_{1},\ldots ,s_{n} \rightarrow State$. The extension to several such operators is straightforward. The theory transformation is of the form $\mathcal {R} \mapsto \mathcal {R}_{ stop }$, where $\mathcal {R}_{ stop }$ is obtained from $\mathcal {R}$ by just adding: (1) a new state constructor operator $[\_,\ldots ,\_] : s_{1},\ldots ,s_{n}\rightarrow State$ to $\varOmega$, and (2) a new rewrite rule $stop : \langle x_{1}\!\! : \!\!s_{1},\ldots , x_{n}\!\! : \!\!s_{n} \rangle \rightarrow [x_{1}\!\! : \!\!s_{1},\ldots , x_{n}\!\! : \!\!s_{n}]$ to R. Also, let $[\,]$ denote the pattern predicate $[x_{1}\!\! : \!\!s_{1},\ldots ,x_{n}\!\! : \!\!s_{n}] \mid \top$. Likewise, for any atomic constrained pattern predicate $B = \langle u_{1},\ldots , u_{n} \rangle \mid \varphi$ we define the pattern predicate $[B] = [u_{1},\ldots , u_{n}] \mid \varphi$ and extend this notation to any union Q of atomic predicates. Since $\langle \_,\ldots ,\_\rangle : s_{1},\ldots ,s_{n}\rightarrow State$ is the only state constructor, we can assume without loss of generality that any atomic constrained pattern predicate in $\mathcal {R}$ is semantically equivalent to one of the form $\langle u_{1},\ldots , u_{n} \rangle \mid \varphi$. Likewise, any pattern predicate will be semantically equivalent to a union of atomic predicates of such form, called in standard form.

Theorem 1

For $S_{0},P \in PatPred (\varOmega ,\varSigma )$ constrained pattern predicates in standard form with $vars (S_{0}) \cap vars (P)= \emptyset$, $\llbracket P \rrbracket$ is an invariant of $(\mathcal {C}_{\mathcal {R}, State },\rightarrow _{\mathcal {R}})$ from $\llbracket S_{0} \rrbracket$ iff $\mathcal {R}_{ stop } \models _{[\,]}^{\forall } S_{0} \rightarrow ^{\circledast } [P]$.

The notion of a parametric invariant can be reduced to the unparameterized one: if $Y= vars (S_{0}) \cap vars (P)$, then $\llbracket P \rrbracket$ is an invariant of $(\mathcal {C}_{\mathcal {R}, State },\rightarrow _{\mathcal {R}})$ from $\llbracket S_{0} \rrbracket$ with parameters Y iff $\mathcal {R}_{ stop } \models _{[\,]}^{\forall } S_{0} \rightarrow ^{\circledast } [P]$. That is, iff $\llbracket P\rho \rrbracket$ is an (unparameterized) invariant of $(\mathcal {C}_{\mathcal {R}, State },\rightarrow _{\mathcal {R}})$ from $\llbracket S_{0} \rho \rrbracket$ for each $\rho \in [Y {{\small \rightarrow }}T_{\varOmega }]$. In this way, Theorem 1 extends to parametric invariants.

Specifying Invariants for QLOCK. Consider the QLOCK specification from Sects. 2 and 3. QLOCK is never terminating. However, we can apply the theory transformation in Theorem 1 by adding an operator $[\_] : Conf \rightarrow State$ and a rule $stop : \, <t> \rightarrow [t]$ for $t\!\!:\!\! Conf$. Define the set of initial states by the pattern predicate $S_0= <n'\ |\ \emptyset \ |\ \emptyset \ |\ nil> \mid dupl (n') \not = tt$. Since QLOCK states have the form $<n\ |\ w\ |\ c\ |\ q>$, mutual exclusion means $|c|\le 1$, which is expressible by the pattern predicate $<n\ |\ w\ |\ i\ |\ i\ ;\ q> \vee <n\ |\ w\ |\ \emptyset \ |\ q>$. But we need also to ensure our multisets are actually sets. Thus, the pattern predicate $P=\big (<n\ |\ w\ |\ i\ |\ i\ ;\ q> \ \! |\ \! dupl ( n\ w\ i )\ne tt \big )\! \vee \! \big ( <n\ |\ w\ |\ \emptyset \ |\ q> \; \! |\; \! dupl ( n\ w )\ne tt \big )$ specifies mutual exclusion. By Theorem 1, QLOCK ensures mutual exclusion from $\llbracket S_{0} \rrbracket$ iff $\mathcal {R}_{ stop } \models _{[\,]}^{\forall } S_{0} \rightarrow ^{\circledast } [P]$.

The following easy corollary can be very helpful in proving invariants. It can, for example, be applied to prove the mutual exclusion of QLOCK.

Corollary 1

Let $S_{0},P \in PatPred (\varOmega ,\varSigma )$ be constrained pattern predicates in standard form with $vars (S_{0}) \cap vars (P)= \emptyset$. $\llbracket P \rrbracket$ is an invariant of $(\mathcal {C}_{\mathcal {R}, State },\rightarrow _{\mathcal {R}})$ from $\llbracket S_{0} \rrbracket$ if: (i) $S_{0} \subseteq P$, and (ii) $\mathcal {R}_{ stop } \models _{[\,]}^{\forall } P \rightarrow ^{\circledast } [P \sigma ]$, where $\sigma$ is a sort-preserving bijective renaming of variables such that $vars (P) \cap vars (P \sigma )= \emptyset$.

Corollary 1 can be extended to parametric invariants (see [13]). The treatment of co-invariants is similar and can also be found in [13].

5 A Sound Inference System

We present our inference system for all-path reachability for any $\mathcal {R}$ satisfying topmost requirements (1)–(2), with rules $R=\{ l_j \rightarrow r_j \ \text {if} \ \phi _j \}_{j \in J}$ such that $l_j , r_j \in T_{\varOmega }(X)$, $j \in J$. Variables of rules in R are always assumed disjoint from variables in reachability formulas; this can be ensured by renaming. The inference system has two proof rules. The $\textsc {Step}^{\forall } + \textsc {Subsumption}$ proof rule allows taking one step of (symbolic) rewriting along all paths according to the rules in $\mathcal {R}$. The Axiom proof rule allows the use of a trusted reachability formula to summarize multiple rewrite steps, and thus to handle repetitive behavior.

These proof rules derive sequents of the form $[\mathcal{A},\ \mathcal{C}] \ \mathrel {\vdash _{T}} \ {{{u} \mathrel {\mid } {\varphi }} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}}$, where $\mathcal A$ and $\mathcal C$ are finite sets of reachability formulas and T a pattern predicate defining a set of T-terminating ground states. Formulas in $\mathcal A$ are called axioms and those in $\mathcal C$ are called circularities. We furthermore assume that in all reachability formulas ${{u} \mathrel {\mid } {\varphi }} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}$ we have $vars (\psi _i) \subseteq vars (v_i) \cup vars ({u} \mathrel {\mid } {\varphi })$ for each i. According to the implicit quantification of the semantic relation $\models _{T}^{\forall }$ this means that any variable in $\psi _i$ is either universally quantified and comes from the precondition ${u} \mathrel {\mid } {\varphi }$, or is existentially quantified and comes from $v_i$ only. This property is an invariant preserved by the two inference rules.

Proofs always begin with a set $\mathcal C$ of formulas that we want to simultaneously prove, so that the proof effort only succeeds if all formulas in $\mathcal C$ are eventually proved. $\mathcal C$ contains the main properties we want to prove as well as any auxiliary lemmas that may be needed to carry out the proof. The initial set of goals we want to prove is $[{\emptyset },\ \mathcal{C}] \ \mathrel {\vdash _{T}} \ \mathcal{C}$, which is a shorthand for the set of goals $\{[{\emptyset },\ \mathcal{C}] \ \mathrel {\vdash _{T}} \ {{{u} \mathrel {\mid } {\varphi }} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}}\ \, {\big |}\ \, ({{u} \mathrel {\mid } {\varphi }} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}) \in \mathcal C\}$. Thus, we start without any axioms $\mathcal A$, but we shall be able to use the formulas in $\mathcal C$ as axioms in their own derivation after taking at least on step with the rewrite rules in $\mathcal {R}$.

A very useful feature is that sequents $[{\emptyset },\ \mathcal{C}] \ \mathrel {\vdash _{T}} \ {{{u} \mathrel {\mid } {\varphi }} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}}$, whose formulas $\mathcal C$ have been postulated (as the conjectures to be proved), are transformed by $\textsc {Step}^{\forall } + \textsc {Subsumption}$ into sequents of the form $[\mathcal{C},\ {\emptyset }] \ \mathrel {\vdash _{T}} \ {{{u'} \mathrel {\mid } {\varphi '}} \longrightarrow ^{\circledast } {\bigvee _i {v'_i} \mathrel {\mid } {\psi '_i}}}$, where now the formulas in $\mathcal C$ can be assumed valid, and can be used in derivations with the Axiom rule.

Verifying QLOCK’s Mutual Exclusion. By Corollary 1, QLOCK’s mutual exclusion can be verified by: (i) using pattern subsumption to check the trivial inclusion $\llbracket S_{0} \rrbracket \subseteq \llbracket P \rrbracket$, and (ii) proving $\mathcal {R}_{ stop } \models _{[\,]}^{\forall } P \sigma \rightarrow ^{\circledast } [P]$, where $\sigma$ is a sort-preserving bijective renaming of variables such that $vars (P) \cap vars (P \sigma )= \emptyset$. But, since for QLOCK, P is a disjunction, in our inference system this means proving from $\mathcal {R}_{ stop }$ that $[\emptyset ,\mathcal {C}] \vdash _{[]} \mathcal {C}$, where $\mathcal {C}$ are the conjectures:

$$<n'\ |\ w'\ |\ i'\ |\ i'\ ;\ q'> \ \! |\ \! \varphi ' \rightarrow ^{\circledast } [<n\ |\ w\ |\ i\ |\ i\ ;\ q> \ \! |\ \! \varphi \vee <n\ |\ w\ |\ \emptyset \ |\ q> \ \! |\ \! \psi ] $$

$$<n'\ |\ w'\ |\ \emptyset \ |\ q'> \ \! |\ \! \psi ' \rightarrow ^{\circledast } [<n\ |\ w\ |\ i\ |\ i\ ;\ q> \ \! |\ \! \varphi \vee <n\ |\ w\ |\ \emptyset \ |\ q> \ \! |\ \! \psi ]. $$

where $\varphi \equiv dupl ( n\ w\ i )\ne tt$, $\psi \equiv dupl ( n\ w )\ne tt$, and $\varphi ',\psi '$ are their obvious renamings.

Before explaining the $\textsc {Step}^{\forall } + \textsc {Subsumption}$ proof rule we introduce some notational conventions. Assume T is the pattern predicate $T= \bigvee _j {t_j} \mathrel {\mid } {\chi _j}$, with $vars (\chi _j) \subseteq vars (t_j)$, and let $R=\{ l_j \rightarrow r_j \ \text {if} \ \phi _j \}_{j \in J}$, we then define:

$$\textsc {match}({u},\ {\{ v_i \}_{i \in I}}) \subseteq \{ (i, \beta ) \mid \beta \in [ vars (v_i) \setminus vars (u) \rightarrow T_\varOmega (X)] \text { s.t. } {u} \mathrel {=}_{E_\varOmega \cup B_\varOmega } {v_i \beta }\}$$

a complete set of (parameter-preserving) $E_{\varOmega } \cup B_{\varOmega }$-matches of u against the $v_i$,

$$\textsc {unify}({{u} \mathrel {\mid } {\varphi '}},\ {R}) \equiv \{ (j, \alpha ) \mid \alpha \in \textit{Unif}_{E_{\varOmega } \cup B_{\varOmega }}(u, l_j) \ \text {and} \ (\varphi ' \wedge \phi _j)\alpha \ \text {satisfiable in} \ \mathcal{T}_{\varSigma /E \cup B}\}$$

a complete set of $E_{\varOmega } \cup B_{\varOmega }$-unifiers of a pattern ${u} \mathrel {\mid } {\varphi '}$ with the lefthand-sides of the rules in R with satisfiable associated constraints.⁴ Consider now the rule:

$\textsc {Step}^{\forall } + \textsc {Subsumption}$

$$ \displaystyle \frac{{\displaystyle \bigwedge _{(j, \alpha ) \in \textsc {unify}({{u} \mathrel {\mid } {\varphi '}},\ {R})} [\mathcal{A\cup \mathcal C},\ {\emptyset }] \ \mathrel {\vdash _{T}} \ {{({r_j} \mathrel {\mid } {\varphi ' \wedge \phi _j}) \alpha } \longrightarrow ^{\circledast } {\bigvee _i ({v_i} \mathrel {\mid } {\psi _i}) \alpha }}}}{{\displaystyle [\mathcal{A},\ \mathcal{C}] \ \mathrel {\vdash _{T}} \ {{{u} \mathrel {\mid } {\varphi }} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}}}} $$

where $\varphi ' \equiv \varphi \wedge \bigwedge _{(i, \beta ) \in \textsc {match}({u},\ {\{ v_i \}})} \lnot (\psi _i \beta )$. This inference rule allows us to take one step with the rules in $\mathcal {R}$. Intuitively, ${u} \mathrel {\mid } {\varphi '}$ characterizes the states satisfying ${u} \mathrel {\mid } {\varphi }$ that are not subsumed by any ${v_i} \mathrel {\mid } {\psi _i}$; that is, states in the lefthand side of the current goal that have not yet reached the righthand side. Note that, according to Definition 4, ${{u} \mathrel {\mid } {\varphi }} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}$ is semantically valid iff ${{u} \mathrel {\mid } {\varphi '}} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}$ is valid. Thus, this inference rule only unifies ${u} \mathrel {\mid } {\varphi '}$ with the lefthand sides of rules in R. We impose on this inference rule a side condition that $\bigvee _{j, \gamma \in \textit{Unif}_{E_{\varOmega } \cup B_{\varOmega }}(u, t_j)} (\varphi ' \wedge \chi _j) \gamma$ is unsatisfiable in $\mathcal{T}_{\varSigma /E \cup B}$, where $T=\bigvee _j {t_j} \mathrel {\mid } {\chi _j}$ is the pattern predicate characterizing the chosen T-terminating states. This condition ensures that any state in ${u} \mathrel {\mid } {\varphi '}$ has an $\mathcal {R}$-successor. Thus, a state in ${u} \mathrel {\mid } {\varphi '}$ reaches on all T-terminating paths a state in $\bigvee _i {v_i} \mathrel {\mid } {\psi _i}$ if all its successors do so. Each $\mathcal {R}$-successor is covered by one of $({r_j} \mathrel {\mid } {\varphi ' \wedge \phi _j}) \alpha$. As an optimization, we check that $(\varphi ' \wedge \phi _j) \alpha$ is satisfiable and we drop the ones which are not. Finally, we also assume that $vars (({u} \mathrel {\mid } {\varphi })\alpha ) \cap vars ((\bigvee _i{v_i} \mathrel {\mid } {\psi _i})\alpha ) = vars (({r_j} \mathrel {\mid } {\varphi ' \wedge \phi _j})\alpha ) \cap vars ((\bigvee _i{v_i} \mathrel {\mid } {\psi _i})\alpha )$. This parameter preservation condition ensures correct implicit quantification. Note that formulas in $\mathcal C$ are added to $\mathcal A$, so that from now on they can be used by Axiom. By using $E_{\varOmega } \cup B_{\varOmega }$-unification, this inference rule performs narrowing of ${u} \mathrel {\mid } {\varphi '}$ with rules R [16].

Axiom

$$ \displaystyle \frac{{\displaystyle \bigwedge _j [{\{ {{u'} \mathrel {\mid } {\varphi '}} \longrightarrow ^{\circledast } {\bigvee _j {v'_j} \mathrel {\mid } {\psi '_j}} \} \cup \mathcal A},\ {\emptyset }] \ \mathrel {\vdash _{T}} \ {{{v'_j \alpha } \mathrel {\mid } {\varphi \wedge \psi '_j \alpha }} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}}}}{{\displaystyle [{\{ {{u'} \mathrel {\mid } {\varphi '}} \longrightarrow ^{\circledast } {\bigvee _j {v'_j} \mathrel {\mid } {\psi '_j}} \} \cup \mathcal A},\ {\emptyset }] \ \mathrel {\vdash _{T}} \ {{{u} \mathrel {\mid } {\varphi }} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}}}} $$

if $\exists \alpha$ such that ${u} \mathrel {=}_{E_\varOmega \cup B_\varOmega } {u' \alpha }$ and $\mathcal{T}_{\varSigma /E \cup B}\mathrel {\models } {\varphi \Rightarrow \varphi ' \alpha }$. This inference rule allows us to use a trusted formula in $\mathcal A$ to summarize multiple transition steps. This is similar to how several transition steps would apply to a ground term, except that for ground terms we would check that $\varphi ' \alpha$ is valid, whereas here we check that the condition $\varphi$ implies $\varphi ' \alpha$. Since $\varphi$ is stronger than $\varphi ' \alpha$, we add $\varphi$ to $({v'_j} \mathrel {\mid } {\psi '_j}) \alpha$ (the result of using axiom ${{u'} \mathrel {\mid } {\varphi '}} \longrightarrow ^{\circledast } {\bigvee _j {v'_j} \mathrel {\mid } {\psi '_j}}$). We assume that ${{u} \mathrel {\mid } {\varphi }} \longrightarrow ^{\circledast } {\bigvee _i {v_i} \mathrel {\mid } {\psi _i}}$ and ${{u'} \mathrel {\mid } {\varphi '}} \longrightarrow ^{\circledast } {\bigvee _j {v'_j} \mathrel {\mid } {\psi '_j}}$ do not share variables, which can always be guaranteed by renaming. For correct implicit quantification, as in $\textsc {Step}^{\forall } + \textsc {Subsumption}$, we assume for each j the parameter preservation condition $vars ({u} \mathrel {\mid } {\varphi }) \! \cap \! vars (\bigvee _i {v_i} \mathrel {\mid } {\psi _i}) = vars ({v'_j \alpha } \mathrel {\mid } {\varphi \wedge \psi '_j \alpha }) \! \cap \! vars (\bigvee _i {v_i} \mathrel {\mid } {\psi _i})$. On a practical note, in order to be able to find the $\alpha$, our implementation requires that $vars (\varphi ') \subseteq vars (u')$, so that all the variables in $vars (\varphi ')$ are matched.

The soundness of $\textsc {Step}^{\forall } + \textsc {Subsumption}$ plus Axiom is now the theorem:

Theorem 2

(Soundness). Let $\mathcal {R}$ be a rewrite theory, and $\mathcal C$ a finite set of reachability formulas. If $\mathcal {R}$ proves $[{\emptyset },\ \mathcal{C}] \ \mathrel {\vdash _{T}} \ \mathcal{C}$ then $\mathcal {R}\models _{T}^\forall \mathcal C$.

Investigating completeness of the logic is left as future work.

6 Prototype Implementation and Experiments

We have implemented the reachability logic proof system in Maude [1]. Our prototype takes as input (i) a rewrite theory $\mathcal {R}=(\varSigma ,E \cup B,R,\phi )$ and (ii) a set of reachability formulas $\mathcal {C} = \{ A_i \rightarrow ^{\circledast } B_i \}_{i \in I}$ to be simultaneously proved.

To mechanize the two proof rules we use a finitary B-unification algorithm as well as an SMT solver to discharge $E\cup B$ constraints. For SMT solving we use variant satisfiability [9, 12], which allows us to handle any rewrite theory $\mathcal {R}=(\varSigma ,E\cup B,R)$ satisfying topmost requirements (1)–(2) and such that the equational theory $(\varSigma ,E\cup B)$ has a convergent decomposition satisfying the finite variant property [2] and protects a constructor subtheory which we assume consists only of commutative and/or AC and/or identity axioms $B_{\varOmega }$. Thus, both validity and satisfiability of QF formulas in the initial algebra $\mathcal {T}_{\varSigma /E \cup B}$ are decidable [9]. Future implementations will support more general rewrite theories, add other decision procedures, and use an inductive theorem prover backend.

We have verified properties for a suite of examples of rewrite theories specifying distributed systems such as communication or mutual exclusion protocols and real-time systems. Table 1 summarizes these experiments. For further details plus runnable code see http://maude.cs.illinois.edu/tools/rltool/.

Table 1. Examples verified in the prototype implementation

Fig. 1.

Partial proof tree for QLOCK

To illustrate how the tool works in practice, Fig. 1 shows a partial derivation of a sequent. Recall that for QLOCK we had to prove $[\emptyset ,\mathcal {C}] \vdash _{[]} \mathcal {C}$, where $\mathcal {C}$ was two already-discussed reachability formulas $G_i\equiv P'_i\rightarrow [P_1]\vee [P_2]$ for $i\in \{1,2\}$ with respective preconditions the renamed disjuncts $P'_{i}$, $1 \le i \le 2$ in invariant $P_{1} \vee P_{2}$, and postcondition $[P_1]\vee [P_2]$, where $P_1\equiv <n\ |\ w\ |\ i\ |\ i\ ;\ q> \ \! |\ \! \textit{dupl}(n\ w\ i)\ne tt$ and $P_2\equiv <n\ |\ w\ |\ \emptyset \ |\ q> \; \! |\; \! \textit{dupl}(n\ w)\ne tt$. Now, consider $[\emptyset ,\mathcal {C}] \vdash _{[]} P'_2\rightarrow ^\circledast [P]$. In the proof fragment below, the initial sequent must apply the step rule. The result of step$(n2w,\theta )$ is the goal resulting from unifying the head of the sequent with the lefthand side of the rule n2w using the unifier $\theta =\{n\mapsto n'' p, w\mapsto w', c\mapsto \emptyset , q\mapsto q'\}$. The next inference axiom$(G_2,\alpha )$ applies axiom $G_2$ using the substitution $\alpha \supseteq \{n\mapsto n^3, w\mapsto w^3, i\mapsto i^3, q\mapsto q^3\}$. Since $G_2$ has two constrained patterns in its succedent, we derive two new goals, represented by proof trees $T_1$ and $T_2$. In either case, we can immediately subsume by noting that our reachability formula’s antecedent is an instance of either $[P_1]$ or $[P_2]$ using substitution $\alpha$, thus terminating the proof.

7 Related Work and Conclusions

This work extends reachability logic [14, 15] to a rewrite-theory-generic logic to reason about both distributed system designs and programs. This extension is non-trivial. It requires: (i) relativizing terminating sequences to a chosen subset $\llbracket T \rrbracket$ of terminating states; (ii) solving the “invariant paradox,” to reason about invariants and co-invariants and characterizing them by reachability formulas through a theory transformation; and (iii) making it possible to achieve higher levels of automation by systematically basing the state predicates on positive Boolean combination of patterns of the form $u \mid \varphi$ with u a constructor term.

In contrast, standard reachability logic [14, 15] uses matching logic, which assumes a first-order model $\mathcal{M}$ and its satisfaction relation $\mathcal{M} \models \varphi$ in its reachability logic proof system. As discusses in Sect. 3, we choose $T_{\varSigma /E \cup B}$ as the model and $\rightarrow _{\mathcal {R}}$ for transitions, rather than some general $\mathcal{M}$ and systematically exploit the isomorphism $T_{\varSigma /E \cup B}|_{\varOmega } \cong T_{\varOmega /E_{\varOmega } \cup B_{\varOmega }}$, allowing us to use unification, matching, narrowing, and satisfiability procedures based on the typically much simpler initial algebra of constructors $T_{\varOmega /E_{\varOmega } \cup B_{\varOmega }}$. This has the advantage that we can explicitly give the complete details of our inference rules (e.g. how $\textsc {Step}^{\forall } + \textsc {Subsumption}$ checks the subsumption, or ensures that states have at least a successor), instead of relying on a general satisfaction relation $\models$ on some $\mathcal{M}$. The result is a simpler logic with only two rules (versus eight in [14, 15]).

We agree with the work in [6] on the common goal of making reachability logic rewrite-theory-generic, but differ on the methods used. Main differences include: (1) [6] does not give an inference system but a verification algorithm. (2) the theories used in [6] assume restrictions like those in [11] for “rewriting modulo SMT,” which limit the class of equational theories. (3) Matching is used in [6] instead of unification. Thus, unless a formula has been sufficiently instantiated, no matching rule may exist, whereas unification with some rule is always possible in our case. (4) No method for proving invariants is given in [6].

In conclusion, the goal of making reachability logic a rewrite-theory-generic verification logic has been advanced. Feasibility has been validated with a prototype and a suite of examples. Building a robust and highly effective reachability logic tool for rewrite theories is a more ambitious future goal.