TY - GEN

T1 - Constructors, sufficient completeness, and deadlock freedom of rewrite theories

AU - Rocha, Camilo

AU - Meseguer, José

N1 - Funding Information:
Acknowledgements. The authors would like to thank Joe Hendrix for fruitful discussions on these ideas and the SCC tool, and the anonymous referees for comments that helped to improve the paper. This work has been partially supported by NSF grants CNS 07-16638 and CCF 09-05584.

PY - 2010

Y1 - 2010

N2 - Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite theory R = (∑, E, R) with equations E and non-equational rules R describing concurrent transitions in a system? This work argues that a rewrite theory naturally has two notions of constructor: the usual one for its equations E, and a different one for its rules R. The sufficient completeness of constructors for the rules R turns out to be intimately related with deadlock freedom, i.e., R has no deadlocks outside the constructors for R. The relation between these two notions is studied in the setting of unconditional order-sorted rewrite theories. Sufficient conditions are given allowing the automatic checking of sufficient completeness, deadlock freedom, and other related properties, by propositional tree automata modulo equational axioms such as associativity, commutativity, and identity. 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 →R associated to a rewrite theory R (and also about the joinability relation ↓R) is both characterized and illustrated with an example.

AB - Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite theory R = (∑, E, R) with equations E and non-equational rules R describing concurrent transitions in a system? This work argues that a rewrite theory naturally has two notions of constructor: the usual one for its equations E, and a different one for its rules R. The sufficient completeness of constructors for the rules R turns out to be intimately related with deadlock freedom, i.e., R has no deadlocks outside the constructors for R. The relation between these two notions is studied in the setting of unconditional order-sorted rewrite theories. Sufficient conditions are given allowing the automatic checking of sufficient completeness, deadlock freedom, and other related properties, by propositional tree automata modulo equational axioms such as associativity, commutativity, and identity. 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 →R associated to a rewrite theory R (and also about the joinability relation ↓R) is both characterized and illustrated with an example.

UR - http://www.scopus.com/inward/record.url?scp=85037546955&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85037546955&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-16242-8_42

DO - 10.1007/978-3-642-16242-8_42

M3 - Conference contribution

AN - SCOPUS:85037546955

SN - 364216241X

SN - 9783642162411

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

SP - 594

EP - 609

BT - Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings

PB - Springer

ER -