Event Structures

Event structures are a truly concurrent model of processes. The following description comes from Mazza 2018:

Amongst all non-interleaving models, event structures (Winskel 1982) are quite appealing, because of their simple and yet very expressive mathematical structure. The basic assumption underlying event structures is that a computational process may be described as a collection of events, which are related by causality and conflict. Causality is an abstraction of time in computation, and allows one to speak of sequentiality and parallelism. Conflict describes non-determinism: If two events are in conflict, we are in front of a choice between the two, as the occurrence of either one of them excludes the occurrence of the other.

Definition

The following definition was sourced from Glynn Winskel's LICS 2005 invited talk.

An event structure (E, \textsf{Con}, \sqsubseteq) comprises

• a set E of events
• a casual dependency relation \sqsubseteq between events
• a set \textsf{Con} \subseteq \mathcal{P}_\text{fin}(E) of finite sets of events

These ingredients must satisfy the following axioms:

• \{ e' \mid e' \sqsubseteq e \} is finite for all e \in E
• \{e\} \in \textsf{Con} for all e \in E
• Y \subseteq X \in \textsf{Con} implies Y \in Con

The idea is that \textsf{Con} holds of finite subsets of events that are consistent between them, and that x \sqsubseteq y encodes that the occurrence of event y causally depends on the occurence of event x.

The configurations \mathcal{C}(E) of an event structure are the subsets X \subseteq E of events which are

• down-closed, i.e. for which e' \sqsubseteq e \in X implies e' \in X
• finitely consistent, i.e. every Y \subseteq_\text{fin} X has Y \in \textsf{Con}
  Configurations stand for histories of events. Down-closure expresses closure under causality: given an event e \in X, X also contains all the events on which e is contingent.

Alternative presentation with conflict relation

The following definition comes from Winskel and Nielsen 1995, and is equivalent to the above (I hope).

Given a poset (P, \sqsubseteq) and a U \subseteq P, write \mathop\downarrow U = \{ b \mid \exists a \in U.\ b \sqsubseteq a \} for the downward closure of U, and write \mathop\downarrow a for the principal ideal \mathop\downarrow \{a\}.

An event structure E = (|E|, \leqslant, \smile) consists of

• a set |E| of events
• a partial order \leqslant on |E|, the causal order
• an irreflexive symmetric relation \smile on E, the conflict relation
  such that

1. for all a \in |E|, the set \mathop\downarrow a is finite
2. if a \smile b \leqslant c then a \smile c

The idea here is that if a \leqslant b, then the event a must happen before the event b does. The first condition then specifies that at most a finite number of events are required to allow a to happen.

Moreover, x \smile y means that x and y are incoherent, incompatible events, which cannot occur concurrently. The relation is irreflexive because events are compatible with themselves. The second condition above says that incompatibility is 'inherited' down the causality chain.

A set U \subseteq |E| is a configuration of E if \mathop\downarrow U = U (closed under causality), and a, b \in U implies that a and b are not in conflict (all events are compatible with each other).

If U is a configuration that does not include a, and U \cup \{ a \} is also a configuration, we say that U enables a (i.e. it contains all the necessary events that must precede a). The smallest configuration that enables a \in |E| is \mathop\downarrow a - \{a\}.

Relationship to domain theory

If the set of events E is countable, then (\mathcal{C}(E), \subseteq) is a dI-domain Winskel 1987, Part 4.

As models of process calculus

As event structures are general models of concurrency, they can be used as "denotational" models of process calculi, such as

• CCS Winskel 1982, or
• the \pi-calculus Crafa et al 2012

We believe they have also been used for CSP, but have not yet tracked down such references.

References

• Event structures were introduced by Glynn Winskel in his thesis:

• The closest to a "textbook" reference is the chapter in the Handbook of Logic in Computer Science by Winskel and Nielsen:

@incollection{winskel_models_1995,
	title = {Models for {Concurrency}},
	volume = {4},
	booktitle = {Handbook of {Logic} in {Computer} {Science}},
	publisher = {Oxford University Press},
	author = {Winskel, Glynn and Nielsen, Mogens},
	year = {1995}
}

• An older presentation can be found in the following chapter and tutorial:

@incollection{winskel_1987,
	address = {Berlin, Heidelberg},
	title = {Event structures},
	volume = {255},
	language = {en},
	booktitle = {Petri {Nets}: {Applications} and {Relationships} to {Other} {Models} of {Concurrency}},
	publisher = {Springer Berlin Heidelberg},
	author = {Winskel, Glynn},
	editor = {Brauer, W. and Reisig, W. and Rozenberg, G.},
	year = {1987},
	doi = {10.1007/3-540-17906-2_31},
	series = {Lecture Notes in Computer Science},
	pages = {325--392}
}

@incollection{winskel_introduction_1989,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {An introduction to event structures},
	number = {354},
	booktitle = {Linear {Time}, {Branching} {Time} and {Partial} {Order} in {Logics} and {Models} for {Concurrency}},
	publisher = {Springer Berlin Heidelberg},
	author = {Winskel, Glynn},
	editor = {de Bakker, J. W. and de Roever, W. -P. and Rozenberg, G.},
	year = {1989},
	doi = {10.1007/BFb0013026},
	pages = {364--397}
}

• Uses of event structures as models for process calculi can be found in

@inproceedings{winskel_1982,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Event structure semantics for {CCS} and related languages},
	volume = {140},
	doi = {10.1007/BFb0012800},
	booktitle = {Automata, {Languages} and {Programming}},
	publisher = {Springer Berlin Heidelberg},
	author = {Winskel, Glynn},
	editor = {Nielsen, Mogens and Schmidt, Erik Meineche},
	year = {1982},
	pages = {561--576}
}

@inproceedings{birkedal_event_2012,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Event {Structure} {Semantics} of {Parallel} {Extrusion} in the {Pi}-{Calculus}},
	volume = {7213},
	doi = {10.1007/978-3-642-28729-9_15},
	booktitle = {Foundations of {Software} {Science} and {Computational} {Structures}},
	publisher = {Springer Berlin Heidelberg},
	author = {Crafa, Silvia and Varacca, Daniele and Yoshida, Nobuko},
	editor = {Birkedal, Lars},
	year = {2012},
	pages = {225--239}
}