Files in this item

FilesDescriptionFormat

application/pdf

main.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-16638NSF grant CCF 09-05584 Date Available in IDEALS: 2010-05-11
﻿