TY - JOUR
T1 - Narrowing and Rewriting Logic
T2 - from Foundations to Applications
AU - Escobar, Santiago
AU - Meseguer, José
AU - Thati, Prasanna
N1 - Funding Information:
Acknowledgments. We cordially thank Catherine Meadows for her fundamental contributions to the security protocol verification ideas that we have summarized as one of the important applications of this work. We thank María Alpuente, Salvador Lucas, and Germán Vidal for their comments about partial evaluation. S. Escobar has been partially supported by the EU (FEDER) and Spanish MEC TIN-2004-7943-C04-02 project, the Generalitat Valenciana under grant GV06/285, and the ICT for EU-India Cross-Cultural Dissemination ALA/95/23/2003/077-054 project. J. Meseguer’s research has been supported in part by ONR Grant N00014-02-1-0715.
PY - 2007/6/1
Y1 - 2007/6/1
N2 - Narrowing was originally introduced to solve equational E-unification problems. It has also been recognized as a key mechanism to unify functional and logic programming. In both cases, narrowing supports equational reasoning and assumes confluent equations. The main goal of this work is to show that narrowing can be greatly generalized, so as to support a much wider range of applications, when it is performed with rewrite theories (Σ, E, R), where (Σ, E) is an equational theory, and R is a collection of rewrite rules with no restrictions. Such theories axiomatize concurrent systems, whose states are equivalence classes of terms modulo E, and whose transitions are specified by R. In this context, narrowing is generalized from an equational reasoning technique to a symbolic model checking technique for reachability analysis of a, typically infinite, concurrent system. We survey the foundations of this approach, suitable narrowing strategies, and various applications to security protocol verification, theorem proving, and programming languages.
AB - Narrowing was originally introduced to solve equational E-unification problems. It has also been recognized as a key mechanism to unify functional and logic programming. In both cases, narrowing supports equational reasoning and assumes confluent equations. The main goal of this work is to show that narrowing can be greatly generalized, so as to support a much wider range of applications, when it is performed with rewrite theories (Σ, E, R), where (Σ, E) is an equational theory, and R is a collection of rewrite rules with no restrictions. Such theories axiomatize concurrent systems, whose states are equivalence classes of terms modulo E, and whose transitions are specified by R. In this context, narrowing is generalized from an equational reasoning technique to a symbolic model checking technique for reachability analysis of a, typically infinite, concurrent system. We survey the foundations of this approach, suitable narrowing strategies, and various applications to security protocol verification, theorem proving, and programming languages.
KW - Equational Reasoning
KW - Maude
KW - Narrowing
KW - Reachability
KW - Rewriting Logic
KW - Security protocols
UR - http://www.scopus.com/inward/record.url?scp=34248646763&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34248646763&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2007.01.004
DO - 10.1016/j.entcs.2007.01.004
M3 - Article
AN - SCOPUS:34248646763
SN - 1571-0661
VL - 177
SP - 5
EP - 33
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - 1
ER -