Constructors, sufficient completeness, and deadlock freedom of rewrite theories

Camilo Rocha, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings
PublisherSpringer-Verlag Berlin Heidelberg
Pages594-609
Number of pages16
ISBN (Print)364216241X, 9783642162411
DOIs
StatePublished - 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6397 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Constructors, sufficient completeness, and deadlock freedom of rewrite theories'. Together they form a unique fingerprint.

Cite this