Narrowing and Rewriting Logic: from Foundations to Applications

13 years 4 months ago

Download users.dsic.upv.es

Narrowing was originally introduced to solve equational E-uniﬁcation 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 conﬂuent 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 speciﬁed 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 inﬁnite, concurrent system. We survey the foundations of this approach, suitable narrowing strategies, and various applications to security pr...

Santiago Escobar, José Meseguer, Prasanna T

Real-time Traffic