Deterministic Behavioural Models for Concurrency (Extended Abstract)

This paper offers three candidates for a deterministic, noninterleaving, behaviour model which generalizes Hoare traces to the noninterleaving situation. The three models are all proved equivalent in the rather strong sense of being equivalent as categories. The models are: deterministic labelled event structures, generalized trace languages in which the independence relation is context-dependent, and deterministic languages of pomsets. Introduction Models for concurrency can be classified according to whether they can represent the structure of systems or just their behaviours (Behaviour or System model); whether they can faithfully take into account the difference between concurrency and nondeterminism (Interleaving or Noninterleaving model); and, finally, whether they can represent the branching structure of processes, i.e., the points in which choices are taken, or not (Linear or Branching Time model). In [9], the authors studied a range of models based on such a classificatio..