Conditional rewriting logic as a unified model of concurrency

Research output: Contribution to journalArticlepeer-review


Rewriting with conditional rewrite rules modulo a set E of structural axioms provides a general framework for unifying a wide variety of models of concurrency. Concurrent rewriting coincides with logical deduction in conditional rewriting logic, a logic of actions whose models are concurrent systems. This logic is sound and complete and has initial models. In addition to general models interpreted as concurrent systems which provide a more operational style of semantics, more restricted semantics with an incresingly denotational flavor such as preorder, poset, cpo, and standard algebraic models appear as special cases of the model theory. This permits dealing with operational and denotational issues within the same model theory and logic. A programming language called Maude whose modules are rewriting logic theories is defined and given denotational and operational semantics. Maude provides a simple unification of concurrent programming with functional and object-oriented programming and supports high level declarative programming of concurrent systems.

Original languageEnglish (US)
Pages (from-to)73-155
Number of pages83
JournalTheoretical Computer Science
Issue number1
StatePublished - Apr 6 1992
Externally publishedYes

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Conditional rewriting logic as a unified model of concurrency'. Together they form a unique fingerprint.

Cite this