BUNDLE EVENT STRUCTURES - A NON-INTERLEAVING SEMANTICS FOR LOTOS

We argue that prime, stable, and flow event structures axe not very practical for providing a semantics for LOTOS as they all have some drawbacks. That is why we introduce 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. We do 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.