Files in this item

FilesDescriptionFormat

application/pdf

application/pdfmain.pdf (627kB)
Technical Report - Updated June 2010PDF

Description

Title:Constructors, Sufficient Completeness and Deadlock Freedom of Generalized Rewrite Theories
Author(s):Rocha, Camilo; Meseguer, José
Subject(s):Rewriting logic
Sufficient completeness
Maude Sufficient Completeness Checker
Rewrite constructors
Equational constructors
Decision procedures
Equational Tree Automata
Maude
Abstract:Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into {\em constructors} and {\em defined} symbols. But what should sufficient completeness mean for a rewrite theory $\rcal = (\Sigma,E,R)$ with equations $E$ and non-equational rules $R$ describing concurrent transitions in a system? The present work argues that a rewrite theory naturally has {\em two} notions of constructor: the usual one for its equations $E$, and a more restrictive one for its rules $R$. The intuition is that a function symbol $f$ that is a constructor for the equations $E$ may be a {\em defined symbol} for the rules $R$. All this can be very useful both to check the completeness of specification with non-equational rules, and for inductive reasoning purposes in rewriting logic. This paper studies the relation between these two notions in the more general case when rewrite theories can have (i) a frozenness map restricting rewriting with $R$, and (ii) a context-sensitive map restricting rewriting with the equations $E$, as it is possible for specifications in the Maude language. It also investigates a syntactic characterization for the notion of deadlock states of a rewrite theory, which appears promising for solving some reachability problems. Sufficient conditions allowing the automatic checking of sufficient completeness, and other related properties, by equational tree automata modulo equational axioms such as as associativity, commutativity, and identity are also given. They are used to extend the Maude Sufficient Completeness Checker from the checking of equational theories to that of both equational and rewrite theories. Finally, the usefulness of the proposed notion of constructors in proving inductive theorems about the reachability rewrite relation $\rightarrow_\rcal$ associated to a rewrite theory $\rcal$ (and also about the joinability relation $\downarrow_\rcal$) is both characterized and illustrated with examples.
Issue Date:2010-05-03
Date Updated:2010-06-21
Genre:Technical Report
Type:Text
Language:English
URI:http://hdl.handle.net/2142/15474
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Sponsor:NSF grant CNS 07-16638
NSF grant CCF 09-05584
Date Available in IDEALS:2010-05-11


This item appears in the following Collection(s)

Item Statistics