TY - JOUR
T1 - Complete symbolic reachability analysis using back-and-forth narrowing
AU - Thati, Prasanna
AU - Meseguer, José
N1 - Funding Information:
We thank Santiago Escobar for many fruitful discussions on the ideas of this paper. We also thank the reviewers for their comments, which have significantly improved the presentation of the paper. This research has been partially supported by ONR Grant N00014-02-1-0715.
PY - 2005
Y1 - 2005
N2 - We propose a method called back-and-forth narrowing for solving reachability goals of the form (∃x→).t1 →* t′1 Λ ... Λ tn → t′n 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. righthand 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.
AB - We propose a method called back-and-forth narrowing for solving reachability goals of the form (∃x→).t1 →* t′1 Λ ... Λ tn → t′n 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. righthand 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.
UR - http://www.scopus.com/inward/record.url?scp=26944493332&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=26944493332&partnerID=8YFLogxK
U2 - 10.1007/11548133_24
DO - 10.1007/11548133_24
M3 - Conference article
AN - SCOPUS:26944493332
SN - 0302-9743
VL - 3629
SP - 379
EP - 394
JO - Lecture Notes in Computer Science
JF - Lecture Notes in Computer Science
T2 - First International Conference on Algebra and Coalgebra in Computer Science, CALCO 2005
Y2 - 3 September 2005 through 6 September 2005
ER -