Complete symbolic reachability analysis using back-and-forth narrowing

Prasanna Thati, José Meseguer

Research output: Contribution to journalConference article

Abstract

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.

Original languageEnglish (US)
Pages (from-to)379-394
Number of pages16
JournalLecture Notes in Computer Science
Volume3629
StatePublished - Oct 26 2005
EventFirst International Conference on Algebra and Coalgebra in Computer Science, CALCO 2005 - Swansea, United Kingdom
Duration: Sep 3 2005Sep 6 2005

Fingerprint

Symbolic Analysis
Reachability Analysis
Concurrent Systems
Decision Procedures
Acoustic waves
Terminate
Term
Reachability
Completeness
Modeling

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Complete symbolic reachability analysis using back-and-forth narrowing. / Thati, Prasanna; Meseguer, José.

In: Lecture Notes in Computer Science, Vol. 3629, 26.10.2005, p. 379-394.

Research output: Contribution to journalConference article

@article{1b488dec1f604344a911a435635312ae,
title = "Complete symbolic reachability analysis using back-and-forth narrowing",
abstract = "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.",
author = "Prasanna Thati and Jos{\'e} Meseguer",
year = "2005",
month = "10",
day = "26",
language = "English (US)",
volume = "3629",
pages = "379--394",
journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Complete symbolic reachability analysis using back-and-forth narrowing

AU - Thati, Prasanna

AU - Meseguer, José

PY - 2005/10/26

Y1 - 2005/10/26

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

M3 - Conference article

AN - SCOPUS:26944493332

VL - 3629

SP - 379

EP - 394

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SN - 0302-9743

ER -