nLab event structure

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 $a \vdash e$ and $b \vdash e$, then either of $a$ or $b$ suffices for $e$ to occur. In a prime event structure, if $a \leq e$ and $b \leq e$ then both $a$ and $b$ must occur before $e$; these are conjunctive causes.

Definition

Definition

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

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

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

• if $X \in \mathrm{Con}$ and $Y \subseteq X$ then $Y \in \mathrm{Con}$;

• if $X \in \mathrm{Con}$, $e \in X$, and $e' \leq e$, then $X \cup \{ e\} \in \mathrm{Con}$.

A restricted but simpler definition is as follows:

Definition

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

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

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

Event structures with binary conflict can be characterised as follows:

Proposition

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

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

$$\forall X \subseteq E. (\forall e, e' \in X. \neg (e \# e')) \implies X \in \mathrm{Con}$$

then defining $\# = \{ (e, e') \mid \{ e, e'\} \in \mathrm{Con} \}$ makes $(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 $E$ for $(E, \leq, \Con)$ whenever possible. The possible states of an event structures are called configurations.

Definition

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

The category of event structures

Definition

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

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

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

There are obvious notions of identity and composition, and we get a category $\mathbf{ES}$ of event structures and maps.

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

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 $f$ is a partial function, and the condition $f(e) = f(e')$ means in particular that they are both defined. Winskel and Nielsen explain this definition as follows:

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

Event structures as presheaves 

Let $\mathbf{P}$ denote the full subcategory of $\mathbf{ES}$ consisting of finite event structures with no conflicts. Equivalently, this is the category of finite posets and (not necessarily monotone) maps that preserve down-closed subsets.

Then the functor

$$\mathbf{ES} \longrightarrow PSh(\mathbf{P})$$

that maps $E$ to the presheaf $P \mapsto \mathbf{ES}(P, E)$ is full and faithful, because the inclusion $\mathbf{P} \hookrightarrow \mathbf{ES}$ is dense.

The essential image of this functor is a subcategory of nonempty separated presheaves (for the Grothendieck topology generated by families of jointly surjective maps) satisfying two additional conditions (see Winskel).

(If we restrict the morphisms in $\mathbf{ES}$ and $\mathbf{P}$ to maps of event structures which are also monotone (these are often called rigid maps) then a similar result holds, and the characterization of the essential image is a bit simpler.)

Event structures with symmetry

Symmetry on an event structure is given by additional structure: an equivalence relation on configurations, such that equivalent configurations are bisimilar. Formally, this is defined in terms of open maps.

Definition

A map $f : E \to E'$ is open if it satisfies a path-lifting condition: writing $\mathbf{P}$ for the subcategory of paths defined above, the condition requires that for $P, Q \in \mathbf{P}$ and a commutative square as in the diagram below, there must be a factorization in terms of two commutative triangles:

Definition

An event structure with symmetry is an event structure $E$ equipped with an internal equivalence relation, i.e. a span

$$E \longleftarrow R \longrightarrow E$$

of jointly monic maps, which is reflexive, symmetric and transitive (this definition uses the fact that $\mathbf{ES}$ has pullbacks), and such that the two legs of the span are open maps.

This can be defined more concretely: an event structure with symmetry is an event structure $E$ equipped with a collection of set-theoretic bijections $\theta : x \cong y$ between configurations of $E$, closed under inverses and compositions and containing all identities (so the set $\mathscr{C}(E)$ of configurations becomes a subcategory of $\mathbf{Set}$, and a groupoid), such that, for every bijection $\theta : x \to y$ in $\mathscr{C}(E)$: * if $x' \subseteq x$ for some configuration $x'$, then the restriction of $\theta$ to $x'$ is also in $\conf{E}$; * if $x \subseteq x'$ for some configuration $x'$, then there is an extension of the bijection $\theta$ to some bijection $\theta' : x' \to y'$ in the symmetry.

We say a map $E \to E'$ preserves symmetry if, for every $\theta : x \cong y$ in the symmetry of $E$, the bijection

$$f x \cong x \cong y \cong f y$$

(determined by the injectivity of $f$ on configurations) is in the symmetry of $E'$. This gives a category $\mathbf{ESS}$ of event structures with symmetry.

Definition

Two parallel maps $f, g : E \to E'$ in $\mathbf{ESS}$ are homotopic (written $f \sim g$) if for every $x \in \mathscr{C}(E)$ the bijection $f x \cong x \cong g x$ (determined by the injectivity on configurations of $f$ and $g$) is in the symmetry of $E'$.

Event structures with symmetry and presheaves

It is shown in Staton & Winskel that with the introduction of symmetry, event structures represent all presheaves over $\mathbf{P}$. Here the functor $\mathbf{ESS} \to \mathrm{PSh}(\mathbf{P})$ takes $E$ to the presheaf $P \mapsto \mathbf{ESS}(P, E)/~$, where we quotient by homotopy of maps.

Relationship with Petri nets

Since they were first described (NPW 81), event structures have been associated with Petri nets. Proofs have been given demonstrating the correspondence between classes of event structure and classes of Petri Net, see, for example, (van Glabbeek & Plotkin).

References

Event structures were introduced in:

• M. Nielsen, G. D. Plotkin, and G. Winskel, Petri nets, event structures and domains, part I, Theoretical Computer Science, vol. 13, pp. 85–108, 1981. doi:10.1016/0304-3975(81)90112-2

Other papers on event structures:

• G. Winskel, Event Structures, in Advances in Petri Nets 1986. Springer Lecture Notes in Computer Science 255, 1987, (pdf).

• 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, Event Structures as Presheaves – Two Representation Theorems BRICS report

• G. Winskel, Event Structures with Symmetry pdf

• 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

• R.J. van Glabbeek, Gordon Plotkin, Configuration Structures, Event Structures and Petri Nets [arXiv:0912.4023]