Petri Nets

Origin. Carl Adam Petri, doctoral thesis "Kommunikation mit Automaten" (1962). The foundational model of concurrency with true (non-interleaving) parallelism. Basis for workflow, protocol, and manufacturing-system analysis; extended into colored, timed, and stochastic variants.

Models. Distributed state and concurrent events. A net is a bipartite graph of places (conditions, holding resources) and transitions (events). Tokens in places encode the current state (marking); transitions fire to move tokens, modeling causality, conflict, and concurrency directly rather than by interleaving.

Formalism.

Structure: A net N = (P, T, F) with places P, transitions T, and flow relation F ⊆ (P×T) ∪ (T×P). Preset •t = {p | (p,t) ∈ F}; postset t• = {p | (t,p) ∈ F}. A marking M : P → ℕ assigns a token count to each place.

Firing rule: Transition t is enabled at M iff M(p) ≥ W(p,t) for all p ∈ •t. Firing yields M′(p) = M(p) − W(p,t) + W(t,p) (weights W on arcs; 1 if unweighted). Written M [t⟩ M′.

Behavioral phenomena: Concurrency: independent transitions fire in any order or "together." Conflict: two transitions share an input token; firing one disables the other. Confusion: interplay of concurrency and conflict.

Analysis notions: Reachability set: markings reachable from M₀. Boundedness: token count bounded (k-bounded; 1-bounded = safe). Liveness: every transition can eventually fire from every reachable marking. Deadlock: a reachable marking enabling no transition. Place/transition invariants from the incidence matrix C = W(t,p) − W(p,t).

Notable subclasses: State machines (each transition one in/out place) and marked graphs (each place one in/out transition). Free-choice nets; colored nets (tokens carry data); timed and stochastic Petri nets.

Symbols.

Symbol	Unicode	Name	Meaning
P	—	Places	Conditions that hold tokens
T	—	Transitions	Events that fire
F	—	Flow relation	Arcs between places and transitions
•	U+2022	Bullet	Prefixed, •t is the preset of t; suffixed, t• is its postset
M	—	Marking	Token distribution over places
[t⟩	—	Firing	M [t⟩ M′: firing t leads from M to M′
W	—	Arc weight	Tokens consumed or produced along an arc
C	—	Incidence matrix	C = W(t,p) − W(p,t)
ℕ	U+2115	Double-struck capital N	Token counts: a marking is M : P → ℕ

Metatheory. Reachability — whether a given marking is reachable from M₀ — is decidable, proved by Mayr (1981) and Kosaraju (1982); its complexity stayed open for four decades until Czerwiński and Orlikowski, and independently Leroux, established Ackermann-hardness in 2021, matching the Ackermann upper bound of Leroux and Schmitz and settling the problem as Ackermann-complete. Coverability and boundedness are sharply characterized: EXPSPACE-hard by Lipton (1976) and in EXPSPACE by Rackoff (1978), with the Karp–Miller coverability tree (1969) supplying a constructive decision procedure that also exposes unbounded places. Liveness is recursively equivalent to reachability (Hack 1974). Equivalence, by contrast, is not decidable at all: Jančar (1995) showed that bisimilarity, and every equivalence between trace equivalence and bisimilarity, is undecidable for labelled nets. Reachability sets need not be semilinear (Hopcroft and Pansiot 1979). Unfoldings give a partial-order semantics, and McMillan's finite complete prefix (1992) turns it into a verification technique.

Applies to. Workflow and business-process modeling (BPMN semantics). Communication protocol verification. Manufacturing and supply-chain systems. Hardware asynchronous circuits. Biochemical reaction networks. Concurrency semantics research.

Limitations. Plain P/T nets cannot test a place for zero, which is simultaneously what keeps their analysis decidable and what bounds their expressiveness; inhibitor arcs restore the test, and two of them already give Turing power, at which point every nontrivial property becomes undecidable. The decidability that remains is not usable as stated, since reachability is Ackermann-complete and coverability EXPSPACE-complete, so the worst case lies beyond any implementation. Invariant methods are sound but incomplete, because reachability sets need not be semilinear. No behavioural equivalence from trace equivalence up to bisimilarity is decidable, so compositional reasoning by equivalence is unavailable. Data, time and probability are absent and require colored, timed or stochastic extensions, each surrendering some decidability; colored nets over infinite color domains are Turing complete. Hierarchy and modularity are likewise extensions rather than features of the model.