Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)

Abstract

Equational unification and matching are fundamental mechanisms in many automated deduction applications. Supporting them efficiently for as wide as possible a class of equational theories, and in a typed manner supporting type hierarchies, benefits many applications; but this is both challenging and nontrivial. We present Maude 3.2’s efficient support of these features as well as of symbolic reachability analysis of infinite-state concurrent systems based on them.

Durán was supported by the grant UMA18-FEDERJA-180 funded by J. Andalucía/FEDER and the grant PGC2018-094905-B-I00 funded by MCIN/AEI/10.13039/501100011033 and ERDF A way of making Europe. Escobar was supported by the EC H2020-EU grant 952215, by the grant RTI2018-094403-B-C32 funded by MCIN/AEI/10.13039/501100011033 and ERDF A way of making Europe, by the grant PROMETEO/2019/098 funded by Generalitat Valenciana, and by the grant PCI2020-120708-2 funded by MICIN/AEI/10.13039/501100011033 and by the European Union NextGenerationEU/PRTR. Martí-Oliet and Rubio were supported by the grant PID2019-108528RB-C22 funded by MCIN/AEI/10.13039/501100011033 and ERDF A way of making Europe. Talcott was partially supported by the U. S. Office of Naval Research under award numbers N00014-15-1-2202 and N00014-20-1-2644, and NRL grant N0017317-1-G002.

1 Introduction

Unification is a key mechanism in resolution [41] and paramodulation-based [36] theorem proving. Since Plotkin’s work [40] on equational unification, i.e., E-unification modulo an equational theory E, it is widely used for increased effectiveness. Since Walther’s work [47] it has been well understood that typed E-unification, exploiting types and subtype hierarchies, can drastically reduce a prover’s search space. Many other automated deduction applications use typed E-unification as a key mechanism, including, inter alia: (i) constraint logic programming, e.g., [12, 23]; (ii) narrowing-based infinite-state reachability analysis and model checking, e.g., [6, 35]; (iii) cryptographic protocol analysis modulo algebraic properties, e.g., [8, 19, 28]; (iv) partial evaluation, e.g., [4, 5]; and (v) SMT solving, e.g., [32, 48]. The special case of typed E-matching is also a key component in all the above areas as well as in: (vi) E-generalization (also called anti-unification), e.g., [1, 2]; and (vii) E-homeomorphic embedding, e.g., [3].

Maximizing the scope and effectiveness of typed E-unification and E-matching means efficiently supporting as wide a class of theories E as possible. Such efficiency crucially depends on both efficient algorithms (and their combinations) and —since the number of E-unifiers may be large— on computing complete minimal sets of solutions to reduce the search space. The recent Maude 3.2 release¹ provides this kind of efficient support for typed E-unification and E-matching in three, increasingly more general classes of theories E:

• 1. Typed B-unification and B-matching, where B is any combination of associativity (A) and/or commutativity (C) and/or unit element (U) axioms.

• 2. Typed $E \cup B$-unification and matching in the user-definable infinite class of theories $E \cup B$ with B as in (1), and $E \cup B$ having the finite variant property (FVP) [13, 21].

• 3. Typed $E \cup B$-unification for the infinite class of user-definable theories $E \cup B$ with B as in (1), and E confluent, terminating, and coherent modulo B.

For classes (1) and (2) the set of B- (resp. $E \cup B$-) unifiers is always complete, minimal and finite, except for the AwoC case when B contains an A but not C axiom for some binary symbol f.² The typing is order-sorted [22, 29] and thus contains many-sorted and unsorted B- (resp. $E \cup B$-) unification as special cases. For class (3), Maude enumerates a possibly infinite complete set of $E \cup B$-unifiers, with the same AwoC exception on B. We discuss new features for classes (1)–(2), and a new narrowing modulo $E \cup B$-based symbolic reachability analysis feature for infinite-state systems specified in Maude as rewrite theories $(\varSigma ,E \cup B,R)$ with equations $E \cup B$ in class (2) and concurrent transition rules R. In Sect. 5 we discuss various applications that can benefit from these new features.

In comparison with previous Maude tool papers reporting on new features —the last one was [16]— the new features reported here include: (i) computing minimal complete sets of most general B- (resp. $E \cup B$-) unifiers for classes (1) and (2) except for the AwoC case; (ii) a new $E \cup B$-matching algorithm for class (2); and (iii) a new symbolic reachability analysis for concurrent systems based on narrowing with transition rules modulo equations $E \cup B$ in class (2) enjoying powerful state-space reduction capabilities based on the minimality and completeness feature (i) and on “folding” less general symbolic states into more general ones through subsumption. Section 3.1 shows the importance of the new $E \cup B$-matching algorithm for efficient computation of minimal $E \cup B$-unifiers.

Notation, Strict-B-Coherence, and FVP. For notation involving either term positions, $p \in pos (t)$, $t|_{p}$, $t[t']_{p}$, or substitutions, $t \theta$, $\theta \mu$, see [14]. Equations $(u=v)\in E$ oriented as rules $(u \rightarrow v)\in \overrightarrow{E}$ are strictly coherent modulo axioms B iff $(t =_{B} t' \wedge t \rightarrow _{\overrightarrow{E},B}w) \Rightarrow \exists w'(t \rightarrow _{\overrightarrow{E},B}w' \wedge w =_{B} w')$, where $t \rightarrow _{\overrightarrow{E},B}w$ iff $\exists (u \rightarrow v)\in \overrightarrow{E},\, \exists \theta , \, \exists p \in pos (t)(u \theta =_{B} t|_{p} \wedge w = t[v \theta ]_{p})$. For $(\varSigma ,E \cup B)$ an equational theory with $\overrightarrow{E}$ confluent, terminating and strictly coherent modulo B, (1) an $\overrightarrow{E},B$-t-variant is a pair $(v,\theta )$ s.t. $v = (t \theta )!_{\overrightarrow{E},B} \wedge \theta = \theta !_{\overrightarrow{E},B}$, where $u !_{\overrightarrow{E},B}$ (resp. $\theta !_{\overrightarrow{E},B})$ denotes the $\overrightarrow{E},B$-normal form of u, resp. $\theta$; (2) for $\overrightarrow{E},B$-t-variants $(v,\theta )$, $(u,\mu )$, the more general relation $(v,\theta ) \sqsupseteq _{B} (u,\mu )$ holds iff $\exists \gamma (u =_{B} v \gamma \wedge \theta \gamma =_{B} \mu )$; (3) $(\varSigma ,E \cup B)$ is FVP [13, 21] iff any $\varSigma$-term t has a finite set of most general $\overrightarrow{E},B$-t-variants. Footnote 5 explains how FVP can be checked.

2 Complete and Minimal Order-Sorted B-Unifiers

Throughout the paper we use the following equational theory $E \cup B$ of the Booleans as a running example (with self-explanatory, user-definable syntax³):

The axioms B are the associativity-commutativity (AC) axioms for xor and and (specified with the assoc comm attributes). The equations E are terminating and confluent modulo B [42]. To achieve strict B-coherence [30], the needed AC-extensions [39] are added —for example, the AC-extension of X xor X = false is X xor X xor Y = Y. The equations E for xor and and define the theory of Boolean rings, except for the missing⁴ distributivity equation X and (Y xor Z) = (X and Y) xor (X and Z). The remaining equations in E define or, not and $\texttt {<=>}$ as definitional extensions. The variant attribute declares that the equation will be used for folding variant narrowing [21]. The theory is FVP,⁵ in class (2). In this section we will consider B-unification (for $B=AC$) using this example. $E \cup B$-unification for the same example will be discussed in Sect. 3.

For B any combination of associativity and/or commutativity and/or identity axioms, Maude’s unify command computes a complete finite set of most general B-unifiers, except for the AwoC case. The new irredundant unify command always returns⁶ a finite, complete and minimal set of B-unifiers, except for the AwoC case. The output of unify for the equation below can be found in [10, §13].

3 $E \cup B$-Unification and Matching for FVP Theories

It is a general result from [21] that if $E \cup B$ is FVP and B-unification is finitary, then $E \cup B$-unification is finitary and a complete finite set of $E \cup B$-unifiers can be computed by folding variant narrowing [21]. Furthermore, assuming that $T_{\varSigma /E,s}$ is non-empty for each sort s, a finitary $E\,\cup \,B$-unification algorithm automatically provides a decision procedure for satisfiability of any positive (the $\wedge ,\vee$-fragment) quantifier-free formula $\varphi$ in the initial algebra $T_{\varSigma /E}$, since $\varphi$ can be put in DNF, and a conjunction of equalities $\varGamma$ is satisfiable in $T_{\varSigma /E}$ iff $\varGamma$ is $E \cup B$-unifiable.

Since for our running example BOOL-FVP the equations $E \cup B$ are FVP and B-unification (in this case $B=AC$) is finitary, all this has useful consequences for BOOL-FVP. Indeed, $T_{\varSigma /E \cup B}$ is exactly the Booleans⁷ on $\{\texttt {true,false}\}$ with the well-known truth tables for and, xor, not, or and $\texttt {<=>}$. This means that $E \cup B$-unification provides a Boolean satisfiability decision procedure for a Boolean expression u on such symbols, namely, u is Boolean satisfiable iff the equation $u = \mathtt{true}$ is $E \cup B$-unifiable. Furthermore, a ground assignment $\rho$ to the variables of u is a satisfying assignment for u iff there exists an $E \cup B$-unifier $\alpha$ of $u = \mathtt{true}$ and a ground substitution $\delta$ such that $\rho = \alpha \delta$. For the same reasons, u is a Boolean tautology iff the equation $u = \mathtt{false}$ has no $E \cup B$-unifiers.

A complete, finite set of $E \cup B$-unifiers can be computed with Maude’s variant unify command whenever $E \cup B$ is FVP, except for the AwoC case. Instead, the new⁸ filtered variant unify command computes a finite, complete and minimal set of $E \cup B$-unifiers, which can be considerably smaller than that computed by variant unify. For our BOOL-FVP example, filtered variant unify gives us a Boolean satisfiability decision procedure plus a symbolic specification of satisfying assignments. Such a procedure is not practical: it cannot compete with standard SAT-solvers; but that was never our purpose: our purpose here is to illustrate with simple examples how $E \cup B$-unification works for the infinite class of user-definable FVP theories $E \cup B$, of which BOOL-FVP is just a simple example; dozens of other examples can be found in [32].

The difference between the variant unify and the new filtered variant unify command is illustrated with the following example; its unfiltered output can be found in [10, §14]. Note that the single $E \cup B$-unifier gives us a compact symbolic description of this Boolean expression’s satisfying assignments.

The computation of a minimal set of $E \cup B$-unifiers relies on filtering by $E\cup B$-matching between two $E\cup B$-unifiers, as explained in the following section.

3.1 FVP $E \cup B$-Matching and Minimality of  $E \cup B$-Unifiers

By definition, a term u $E \cup B$-matches another term v iff there is a substitution $\gamma$ such that $u =_{E \cup B} v \gamma$. Besides the existing match command modulo axioms B, Maude’s new variant match command computes a complete, minimal set of $E \cup B$-matching substitutions for any FVP theory $E \cup B$ in class (2), except for the AwoC case. Such an algorithm could always be derived from an $E \cup B$-unification algorithm by replacing u by $\overline{u}$, where all variables in u are replaced by fresh constants in $\overline{u}$, and computing the $E \cup B$-unifiers of $\overline{u} = v$. But a more efficient special-purpose algorithm has been designed and implemented for this purpose. $E \cup B$-matching algorithms are automatically provided by Maude for any user-definable theory in class (2) with the variant match command.

This is a good moment to ask and answer a relevant question: Why is computing a complete minimal set of $E \cup B$-unifiers for a unification problem $\varGamma$, where $E \cup B$ is an FVP theory in class (2) except for the AwoC case, nontrivial? We first need to explain how minimality is achieved. Suppose that $\alpha$ and $\beta$ are two $E \cup B$-unifiers of a system of equations $\varGamma$ with, say, typed variables $x_{1},\ldots , x_{n}$. We then say that $\alpha$ is more general than $\beta$ modulo $E \cup B$, denoted $\alpha \sqsupseteq _{E \cup B} \beta$, iff there is a substitution $\gamma$ such that for each $x_{i}$, $1 \le i \le n$, $\gamma (\alpha (x_{i})) =_{E \cup B} \beta (x_i)$. But this exactly means that the vector $[\beta (x_{1}),\ldots ,\beta ( x_{n})]$ $E \cup B$-matches the vector $[\alpha (x_{1}),\ldots ,\alpha ( x_{n})]$ with $E \cup B$-matching substitution $\gamma$. A complete set of $E \cup B$-unifiers of $\varGamma$ is by definition minimal iff for any two different unifiers $\alpha$ and $\beta$ in it we have $\alpha \not \sqsupseteq _{E \cup B} \beta$ and $\beta \not \sqsupseteq _{E \cup B} \alpha$, i.e., the two associated $E \cup B$-matching problems fail.

What is nontrivial is computing a minimal complete set of $E \cup B$-unifiers efficiently. One could do so inefficiently by simulating $E \,\cup \, B$-matching with $E \cup B$-unification, and more efficiently by using an $E \cup B$-matching algorithm. Maude achieves still greater efficiency by directly computing the $\alpha \sqsupseteq _{E \,\cup \, B} \beta$ relation. The key difference between the variant unify command and the new filtered variant unify command is that the second computes a $E \cup B$-minimal set of $E \cup B$-unifiers of $\varGamma$ using the $\alpha \sqsupseteq _{E \cup B} \beta$ relation, whereas the first only computes a set of B-minimal $E \cup B$-unifiers of $\varGamma$ using the cheaper $\alpha \sqsupseteq _{B} \beta$ relation. There are three ideas we use to make it fast in practice: (i) variant matching is faster than variant unification because one side is variable-free; (ii) enumerating the variant matchers between two variant unifiers is far more expensive than checking existence of a matcher; and (iii) variant unifiers are discarded on-the-fly avoiding further narrowing steps and computation.

4 Narrowing-Based Symbolic Reachability Analysis

In Maude, concurrent systems are specified in so-called system modules as rewrite theories of the form: $\mathcal {R}= (\varSigma ,G,R)$, where G is an equational theory either of the form B in class (1), or $E \cup B$ in classes (2) or (3), and R are the system transition rules, specified as rewrite rules. When the theory $\mathcal {R}$ is topmost, meaning that the rules R rewrite the entire state, narrowing with rules R modulo the equations G is a complete symbolic reachability analysis method for infinite-state systems [35]. That is, given a term u with variables $\overrightarrow{x}$, representing a typically infinite set of initial states, and another term v with variables $\overrightarrow{y}$, representing a possibly infinite set of target states, narrowing can answer the question: can an instance of u reach an instance of v? That is, does the formula $\exists \overrightarrow{x},\overrightarrow{y}\;\; u \rightarrow ^{*} v$ hold in $\mathcal {R}$? Note that, if the complement of a system invariant I can be symbolically described as the set of ground instances of terms in a set $\{v_{1},\ldots , v_{n}\}$ of pattern terms, then narrowing provides a semi-decision procedure for verifying whether the system specified by $\mathcal {R}$ fails to satisfy I starting from an initial set of states specified by u. Namely, I holds iff no instance of any $v_{i}$ can be reached from some instance of u.

Assuming G is in class (1) or (2), Maude’s vu-narrow command implements narrowing with R modulo G by performing G-unification at each narrowing step. However, the number of symbolic states that need to be explored can be infinite. This means that if no solution exists for the narrowing search, Maude will search forever, so that only depth-bounded searches will terminate. The great advantage of the new {fold} vu-​narrow {filter,delay} command is that it performs a powerful symbolic state space reduction by: (i) removing a newly explored symbolic state $v'$ if it $E \cup B$-matches a previously explored state v and replacing transition with target $v'$ by transitions with target v; and (ii) using minimal sets of $E \cup B$-unifiers for each narrowing step and for checking common instances between a newly explored state and the target term (ensured by words filter and delay). This can make the entire search space finite and allow full verification of invariants for some infinite-state systems. Consider the following Maude specification of Lamport’s bakery protocol.

The states of BAKERY have the form “m | x? | PS" with m the ticket-dispensing counter, x? the (possibly locked) counter to access the critical section, and PS a multiset of processes either waiting or in the critical section. BAKERY is infinite-state: [new] creates new processes, and the counters can grow unboundedly. When a waiting process enters the critical section with [enter], the second counter n is locked as [n]; and it is unlocked and incremented when it leaves it with [leave]. The key invariant is mutual exclusion. Note that the term “$\texttt {i ~|~ x?~ |~< crit, j> \,< crit, k> PS}$” describes all states in the complement of mutual exclusion states. Without the fold option, narrowing does not terminate, but with the following command we can verify that BAKERY satisfies mutual exclusion, not just for the initial state “0 | 0 | mt", but for the much more general infinite set of initial states with waiting processes only “m | n | WPS".

The new vu-​narrow {filter,delay} command can achieve dramatic state space reductions over the previous vu-​narrow command by filtering $E \cup B$-unifiers. This is illustrated by a simple cryptographic protocol example in [10, §15] exploiting the unitary nature of unification in the exclusive-or theory [24].

5 Applications and Conclusion

Maude can be used as a meta-tool to develop new formal tools because: (i) its underlying equational and rewriting logics are logical —and reflective meta-logical— frameworks [7, 27, 46]; (ii) Maude’s efficient support of logical reflection through its META-LEVEL module; (iii) Maude’s rewriting, search, model checking, and strategy language features [11, 15]; and (iv) Maude’s symbolic reasoning features [15, 33], the latest reported here. We refer to [11, 15, 31, 33] for references on various Maude-based tools. Many of them can benefit from these new features.

By way of example we mention some areas ready to reap such benefits: (1) Formal Analysis of Cryptographic Protocols. The new features can yield substantial improvements to tools such as Maude-NPA [19], Tamarin [28] and AKISS [8]. (2) Model Checking of Infinite-State Systems. The narrowing-based LTL symbolic model checker reported in [6, 20], and the addition of new symbolic capabilities to Real-Time Maude [37, 38] can both benefit from the new features. (3) SMT Solving. In Sect. 3 we noted that FVP $E \cup B$-unification makes satisfiability of positive QF formulas in $T_{\varSigma /E \cup B}$ decidable. Under mild conditions, this has been extended in [32, 44] to a procedure for satisfiability in $T_{\varSigma /E \cup B}$ of all QF formulas which will also benefit from the new features. (4) Theorem Proving. The new Maude Inductive Theorem Prover under construction [34], as well as Maude’s Invariant Analyzer [43] and Reachability Logic Theorem Prover [45] all use equational unification and narrowing modulo equations; so all will benefit from the new features. (5) Theory Transformations based on equational unification, e.g., partial evaluation [4], ground confluence methods [17] or program termination methods [25, 26] could likewise become more efficient.

In conclusion, we have presented and illustrated with examples new equational unification and matching, and symbolic reachability analysis features in Maude 3.2. Thanks to the above-mentioned properties (i)–(iv) of Maude as a meta-tool, we hope that this work will encourage other researchers to use Maude and its symbolic features to develop new tools in many different logics.