eventstructure

An event structure is a formal model used in the theory of concurrency to represent the causal, concurrent, and nondeterministic behavior of systems. It consists of a set of events together with relations that encode how events depend on or exclude one another. Event structures provide a way to reason about possible executions without prescribing a single global timeline.

In the standard definition, an event structure consists of a set E of events, a partial order ≤ on E representing causality (if e' ≤ e, then e' must occur before e), and a symmetric, irreflexive conflict relation # on E indicating mutual exclusion between events. In some variants, enabling relations or stability properties are added to capture different modeling assumptions. In prime event structures, the conflict relation is hereditary: if e # f and g ≤ e, then g # f.

A configuration is a set C ⊆ E that is downward closed with respect to ≤ (every cause of an event in C is also in C) and conflict-free (no two distinct events in C are in conflict). Configurations represent possible consistent runs or executions. The set of all configurations forms the domain of the model and can be ordered by inclusion to reflect refinement of runs.

Variants and applications: Prime event structures are a common form where each event has a unique set of minimal causes; more general stable or connected variants relax some constraints. Event structures underpin the true-concurrency semantics of programming languages, and they relate to Petri nets via net unfoldings. They are used in domain theory to connect operational behavior with semantic models.