Open Systems Laboratory at Illinois

Complete symbolic reachability analysis using back-and-forth narrowing

By Prasanna Thati and José Meseguer. Theor. Comput. Sci, 366(1-2):163–179, 2006.

Publisher Link:


We propose a method called back-and-forth narrowing for solving reachability goals of the form in general term rewrite systems. The method is a complete semi-decision procedure in the sense that it is guaranteed to find a solution when one exists, but in general it may not terminate when there are no solutions. The completeness result is very general in that it makes no assumptions about the given term rewrite system. Specifically, the rewrite rules need not be linear, confluent, or terminating, and can even have extra-variables in the right-hand side. Such generality is often essential while modeling concurrent systems or axiomatizing inference systems as rewrite rules, and in such applications back-and-forth narrowing can be used as a sound and complete technique for symbolic reachability analysis or as a deductive procedure for proving existential formulae.


    author = "Thati, Prasanna and Meseguer, José",
    title = "Complete symbolic reachability analysis using back-and-
             forth narrowing",
    ee = "",
    journal = "Theor. Comput. Sci",
    keywords = "formal methods",
    number = "1-2",
    pages = "163-179",
    volume = "366",
    year = "2006",