nLab
event structure

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.

Original form

Definition

An event structure, (E,,)(E,\le, \sharp), consists of a poset (E,)(E,\le) of events, where the partial order relation expresses causal dependency, together with a symmetric irreflexive relation \sharp, called incompatibility . This data is to satisfy

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

and

  • hereditary incompatibility: for any e,e,eEe,e',e'' \in E, eee\sharp e' and eee'\le e'' implies eee\sharp e''.
Definition

Let 𝔼=(E,,)\mathbb{E} = (E,\le, \sharp) be an event structure. Define its set of configurations, C(𝔼)=C(E,,)C(\mathbb{E}) = C(E,\le, \sharp), to consist of those subsets XEX \subseteq E, which are

  • conflict-free: if e,eXe, e'\in X then ¬(ee)\neg (e\sharp e'),

and

  • downward closed: if eXe\in X, eX\downarrow e\subseteq X.

A morphism f:𝔼𝔼f : \mathbb{E}\to \mathbb{E}' of event structures consists of a partial function f:EEf : E \to E' such that

  • if XC(𝔼)X\in C(\mathbb{E}), then f(X)C(𝔼)f(X) \in C(\mathbb{E}')

and

  • if e 0e_0 and e 1e_1 are in XX with both f(e 0)f(e_0) and f(e 1)f(e_1) defined and f(e 0)=f(e 1)f(e_0)=f(e_1) then e 0=e 1e_0 = e_1.

Gloss

This second condition says that if both f(e 0)f(e_0) and f(e 1)f(e_1) are defined and either f(e 0)f(e 1)f(e_0)\sharp' f(e_1) or f(e 0)=f(e 1)f(e_0)=f(e_1), then either e 0e 1e_0\sharp e_1, or e 0=e 1e_0 = e_1.

Winskel and Neilsen explain the definition as follows:

A morphism f:𝔼𝔼f : \mathbb{E}\to \mathbb{E}' between event structures expresses how behaviour in 𝔼\mathbb{E} determines behaviour in 𝔼\mathbb{E}'. The partial function, ff, expresses how the occurrence of an event in 𝔼\mathbb{E} implies the simultaneous occurrence of an event in 𝔼\mathbb{E}'; 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 𝔼\mathbb{E} have the same image in 𝔼\mathbb{E}' under ff then they cannot belong to the same configuration.

(There is more discussion of the notion of morphism of event structures in the notes referred to below.)

With this definition of morphism, we get the category, ES\mathbf{ES} of event structures.

Alternative form

In some sources, rather than stress the inconsistency relation, the complementary consistency relation. This leads to the definition of a family, ConCon, of finite subsets of EE, which satisfy

  • {e}E\{e\}\in E for all eEe\in E;

  • YXConY\subseteq X\in Con implies YConY\in Con,

and

  • XConX\in Con and eeXe\leq e'\in X then X{e}ConX\cup \{e\}\in Con.

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).

  • G. Winskel and S. Staton, On the expressivity of symmetry in event structures, LICS 2010

Revised on December 23, 2010 07:27:05 by Toby Bartels (173.190.146.220)