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.
The following definition was sourced from Glynn Winskel's LICS 2005 invited talk.
An event structure comprises
These ingredients must satisfy the following axioms:
The idea is that holds of finite subsets of events that are consistent between them, and that encodes that the occurrence of event causally depends on the occurence of event .
The configurations of an event structure are the subsets of events which are
The following definition comes from [Winskel and Nielsen 1995], and is equivalent to the above (I hope).
Given a poset and a , write for the downward closure of , and write for the principal ideal .
An event structure consists of
The idea here is that if , then the event must happen before the event does. The first condition then specifies that at most a finite number of events are required to allow to happen.
Moreover, means that and 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 is a configuration of if (closed under causality), and implies that and are not in conflict (all events are compatible with each other).
If is a configuration that does not include , and is also a configuration, we say that enables (i.e. it contains all the necessary events that must precede ). The smallest configuration that enables is .
If the set of events is countable, then is a dI-domain [Winskel 1987, Part 4].
As event structures are general models of concurrency, they can be used as "denotational" models of process calculi, such as
We believe they have also been used for CSP, but have not yet tracked down such references.
Winskel, Glynn. 1980. ‘Events in Computation’. PhD Thesis, University of Edinburgh.
[pdf]
Winskel, Glynn, and Mogens Nielsen. 1995. ‘Models for Concurrency’. In Handbook of Logic in Computer Science. Vol. 4. Oxford University Press. [pdf]
@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}
}
Winskel, Glynn. 1987. ‘Event Structures’. In Petri Nets: Applications and Relationships to Other Models of Concurrency, edited by W. Brauer, W. Reisig, and G. Rozenberg, 255:325–92. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-17906-2_31. [pdf]
@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}
}
Winskel, Glynn. 1989. ‘An Introduction to Event Structures’. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, edited by J. W. de Bakker, W. -P. de Roever, and G. Rozenberg, 364–97. Lecture Notes in Computer Science 354. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/BFb0013026. [pdf]
@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}
}
Winskel, Glynn. 1982. ‘Event Structure Semantics for CCS and Related Languages’. In Automata, Languages and Programming, edited by Mogens Nielsen and Erik Meineche Schmidt, 140:561–76. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/BFb0012800.
@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}
}
Crafa, Silvia, Daniele Varacca, and Nobuko Yoshida. 2012. ‘Event Structure Semantics of Parallel Extrusion in the Pi-Calculus’. In Foundations of Software Science and Computational Structures, edited by Lars Birkedal, 7213:225–39. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-28729-9_15.
@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}
}