Rewriting logic can naturally express both concurrent computation and logical deduction and is thus applied in system specification and verification. Here, a core question is whether, from an initial state, the execution of the system may reach another state satisfying some condition. In rewriting logic, both state descriptions can be formalized by terms with free variables such that reachability denotes the existence of a sequence of rewrite steps. A method called narrowing, originally devised for the solution of term equations (unification), has been extended to also cover the reachability problem.

The authors’ previous work extended narrowing to conditional rewriting (where rules may have side conditions) and implemented the calculus in the software system Maude. The present paper builds upon this by introducing two improved calculi for unification and reachability that cover a larger class of rewrite theories than before. Furthermore, these calculi apply the optimization technique of sentence normalized rewriting that yields canonical versions of the terms before each narrowing step, thus reducing the search space and speeding up the computation.

The core of the paper formalizes the new calculi and proves their soundness and completeness. This presentation is made accessible by the running example of a specification that illustrates the definitions; ultimately it is shown how a particular reachability goal is solved from a Maude specification of this example. While the new calculi have not been implemented yet, future work will investigate their connection with external constraint solvers to further improve the performance of any implementation.