Bundle Event Structures: A Non-Interleaving Semantics for LOTOS

摘要

The author argues that prime, stable, and flow event structures are not verypractical for providing a semantics for LOTOS as they all have some drawbacks. Therefore, he introduces bundle event structures as labelled event structures with a binary conflict relation and a so-called bundle set instead of a causality, precedence or flow relation. Bundle event structures have an attractive graphical representation; the analysis is facilitated by providing several equivalence laws. Like in flow and stable event structures, events can be enabled in different ways. There are no self-conflicting events like in flow event structures. The author does allow so-called impossible events that can never happen but can always be removed (unlike self-conflicting events in flow event structures). A bundle event structure semantics is given for a Basic LOTOS subset containing all operators except disabling and process instantiation. This semantics is proven correct with respect to a simple event transition system.