Abstract
We present an w-complete algebra of a class of deterministic event structures which are labelled prime event structures where the labelling function satises a certain distinctness condition. The operators of the algebra are summation sequential composition and join. Each of these gives rise to a monoid in addition a number of distributivity properties hold Summation loosely corresponds to choice and join to parallel composition with however some nonstandard aspects The space of models is a complete partial order in fact a complete lattice, in which all operators are continuous hence minimal fixpoints can be defined inductively. Moreover the submodel relation can be captured within the algebra by summation x \sqsubseteq y iff x + y = y; therefore, the effect of fixpoints can be captured by an infinitary proof rule, yielding a complete proof system for recursively defined deterministic event structures.
Original language | English |
---|---|
Pages | 160-174 |
Number of pages | 15 |
DOIs | |
Publication status | Published - 1995 |
Event | 6th International Conference on Concurrency Theory, CONCUR 1995 - Philadelphia, United States Duration: 21 Aug 1995 → 24 Aug 1995 Conference number: 6 |
Conference
Conference | 6th International Conference on Concurrency Theory, CONCUR 1995 |
---|---|
Abbreviated title | CONCUR |
Country/Territory | United States |
City | Philadelphia |
Period | 21/08/95 → 24/08/95 |
Keywords
- IR-66652
- EWI-8271