nLab
event structure

Contents

Contents

Idea

Event structures were introduced in order to abstract away from the precise ‘places’ and times at which events occur in distributed systems. The structure focuses on the events and the causal ordering between them.

Event structures in the sense of this article are sometimes also called prime event structures. There are other variants, for example where the partial order \leq is replaced by an enabling relation \vdash. This is usually more expressive, because an event can have disjunctive causes: if aea \vdash e and beb \vdash e, then either of aa or bb suffices for ee to occur. In a prime event structure, if aea \leq e and beb \leq e then both aa and bb must occur before ee; these are conjunctive causes.

Definition

Definition

An event structure is a tuple (E,,Con)(E,\leq, \mathrm{Con}) consisting of a poset (E,)(E,{\le}) of events, and a nonempty set Con𝒫(E)\mathrm{Con} \subseteq \mathcal{P}(E) of consistent subsets, satisfying the following axioms:

  • finite causes: for every event ee the set {eee}\{e'\mid e'\le e\} is finite;

  • if eEe \in E then {e}Con\{ e \} \in \mathrm{Con};

  • if XConX \in \mathrm{Con} and YXY \subseteq X then YConY \in \mathrm{Con};

  • if XConX \in \mathrm{Con}, eXe \in X, and eee' \leq e, then X{e}ConX \cup \{ e\} \in \mathrm{Con}.

A restricted but simpler definition is as follows:

Definition

An event structure with binary conflict is a tuple (E,,#)(E, \leq, \#), where (E,)(E, {\leq}) is a poset and #\# is an irreflexive binary relation on EE, the conflict relation, satisfying:

  • finite causes: for every event ee the set {eee}\{e'\mid e'\le e\} is finite;

  • hereditary conflict: if e#ee \# e' and eee' \leq e'' then e#ee \# e''.

Event structures with binary conflict can be characterised as follows:

Proposition

If (E,,#)(E, \leq, \#) is an event structure with binary conflict, then defining Con={XEe,eX.¬(e#e)}\mathrm{Con} = \{ X \subseteq E \mid \forall e, e' \in X. \neg (e \# e') \} makes (E,,Con)(E, \leq, \Con) an event structure.

Conversely, if an event structure (E,,Con)(E, \leq, \mathrm{Con}) satisfies

XE.(e,eX.¬(e#e))XCon \forall X \subseteq E. (\forall e, e' \in X. \neg (e \# e')) \implies X \in \mathrm{Con}

then defining #={(e,e){e,e}Con}\# = \{ (e, e') \mid \{ e, e'\} \in \mathrm{Con} \} makes (E,,#)(E, \leq, \#) an event structure with binary conflict.

That is, event structures with binary conflict correspond to event structures in which pairwise consistency implies mutual consistency.

We write EE for (E,,Con)(E, \leq, \Con) whenever possible. The possible states of an event structures are called configurations.

Definition

Let EE be an event structure. A configuration of EE is a subset xEx \subseteq E which is consistent (xConx \in \Con) and down-closed (if exe\in x and eee' \leq e then exe' \in x). The set of \emph{finite} configurations of EE is denoted 𝒞(E)\mathscr{C}(E).

The category of event structures

Definition

A (total) map of event structures from (E,,Con)(E, \leq, \Con) to (E,,Con)(E', \leq', \Con') is a function f:EEf : E \to E' such that:

  • ff preserves configurations: if x𝒞(E)x\in \mathscr{C}(E), then f(x)𝒞(E)f(x) \in \mathscr{C}(E').

  • ff is locally injective: if e,ex𝒞(E)e, e' \in x \in \mathscr{C}(E) and f(e)=f(e)f(e) = f(e'), then e=ee = e'.

Intuitively, a map EEE \to E' expresses that all executions of EE can be faithfully simulated within EE'.

Partial maps of event structures are also important in the literature, for example in the event structure model of CCS. The definition is the same when ff is a partial function, and the condition f(e)=f(e)f(e) = f(e') means in particular that they are both defined. Winskel and Nielsen explain this definition as follows:

A morphism f:EEf : E\to E' between event structures expresses how behaviour in EE determines behaviour in EE'. The partial function, ff, expresses how the occurrence of an event in EE implies the simultaneous occurrence of an event in EE'; the fact that f(e)=ef(e) = e' can be understood as expressing that the event ee is a ‘’component’‘ of the event ee' and, in this sense, that the occurrence of ee implies the simultaneous occurrence of ee'. If two distinct events in EE have the same image in EE' under ff then they cannot belong to the same configuration.

With this definition of morphism, and the obvious notions of identity and composition, we get the category ES\mathbf{ES} of event structures (and total maps).

Event structures as presheaves 

References

  • G. Winskel and M. Nielsen, Models for concurrency. vol. 3, Handbook of Logic in Computer Science, pages 100 - 200, Oxford Univ. Press, 1994. (see also online technical report).

  • G. Winskel, Events, causality, and symmetry, (an earlier version appeared in the BCS conference ‘Visions in Computer Science.’ September 2008. The final version appears in a special issue of The Computer Journal 2009; doi: 10.1093/comjnl/bxp052; see also an online version).

  • Sam Staton and G. Winskel, On the expressivity of symmetry in event structures,

    LICS 2010

Last revised on July 13, 2021 at 05:11:24. See the history of this page for a list of all contributions to it.