Conditional rewriting logic as a unified model of concurrency (Q1190488)

This work attempts to clearify the notion of a concurrent system by proposing a model theory for deduction, i.e., the proof theory of rewriting. The 82 pages of the paper are organized in 6 sections which are shortly described as follows: In the first section it is argued why and how rewriting logic is a logic of action and, as such, being intrinsically of concurrent nature. Section 2 contains the basics of rewriting and the rule of (concurrent) deduction are given. The semantics is given in Secion 3 by interpreting the rewriting rules as rules of generation. The initial model is proven to be sound and complete. Section 4 proposes the language MAUDE which includes OBJ-3 and serves as a semantics of rewrite rule programs as concurrent systems. Section 5 shows in detail how many well known concurrent systems can be viewed as concurrent rewriting systems. The 5 sections are completed with a discussion of related work and a list of 125 references.