Petri Nets: Tokens, Workflows, and Decidable Soundness

Carl Adam Petri introduced the nets in his 1962 dissertation, Kommunikation mit Automaten, a decade before the process calculi. The model has outlived most of its successors for one reason: it draws concurrency rather than encoding it. Precedence, synchronisation and resource contention are visible in the graph, and for the workflow specialisation, correctness of the whole task graph is decidable.

The token game

A Petri net is a bipartite graph $N = (P, T, F)$: places $P$ (drawn as circles), transitions $T$ (bars), and arcs $F \subseteq (P \times T) \cup (T \times P)$. State is a marking $M : P \to \mathbb{N}$, a distribution of tokens over places. Writing $\bullet t$ for the input places of $t$ and $t \bullet$ for its outputs, a transition is enabled when every input place holds a token, and firing moves them:

That is the entire semantics. The three coordination phenomena fall out of the graph shape directly:

• Precedence. A place between two transitions is an obligation: the second cannot fire until the first has produced the token.
• Synchronisation. A transition with several input places is an AND-join. It waits, structurally, for all of them.
• Contention. Two transitions sharing an input place are in conflict: one token, two claimants, and firing either disables the other. A resource is just a place whose token is borrowed and returned.

Interleaving models recover these with auxiliary machinery (locks, guards, fairness assumptions). In a net they are the primitive vocabulary, and concurrency is a partial order on firings rather than a shuffle of traces.

Watching a net run

The net below is an order-fulfilment workflow. receive splits a case into two concurrent checks; both need the single resource token in $R$; dispatch joins the branches.

Every claim in the previous section is on screen: the split, the conflict at $R$, the join idling until both $p_3$ and $p_4$ are marked.

Why the questions are answerable

Petri nets are not Turing-complete. A transition can test for the presence of a token but not its absence, and that single weakness is load-bearing: reachability of a marking is decidable (Mayr, 1981), with the exact complexity settled only in 2021 as Ackermann-complete. Boundedness and coverability are EXPSPACE-complete (Lipton; Rackoff), and liveness reduces to reachability. Add inhibitor arcs, which test for zero, and the model becomes Turing-complete and every one of these questions undecidable.

Contrast the π-calculus from the previous post: mobility makes it Turing-complete, so behavioural questions are undecidable in general and one falls back on types or bisimulation proofs. Petri nets take the opposite bargain. The topology is frozen at design time, and the payment for that rigidity is algorithmic verification.

Workflow nets and soundness

Van der Aalst’s workflow nets (1997) specialise the model to business processes: one source place $i$, one sink place $o$, every node on a path from $i$ to $o$. A case is a token injected at $i$; the process is correct when it is sound:

1. Option to complete. From every marking reachable from $\lbrace i \rbrace$, the marking $\lbrace o \rbrace$ remains reachable.
2. Proper completion. When $o$ is marked, nothing else is: no orphaned work survives the case.
3. No dead transitions. Every task can occur in some run.

The central theorem: a workflow net is sound iff the short-circuited net, obtained by adding a transition feeding $o$ back to $i$, is live and bounded. Both properties are decidable, so soundness is a decidable property of the task graph, checked before any case runs. No deadlock hunt, no test suite over interleavings; the diagram itself is the proof obligation, and tools such as Woflan discharge it. For free-choice nets, the class most modelling notations compile into, the check is polynomial.

This is the result that makes the model industrial. BPMN and the workflow patterns literature sit on workflow nets; YAWL was built on them outright. When an orchestration language offers you a static guarantee that every process instance can finish, a soundness checker is what is running underneath.

Further reading

Murata’s survey “Petri Nets: Properties, Analysis and Applications” (Proceedings of the IEEE, 1989) remains the standard technical entry point. Reisig’s Understanding Petri Nets (Springer, 2013) is the gentler book-length treatment. For the workflow specialisation, van der Aalst’s “The Application of Petri Nets to Workflow Management” (Journal of Circuits, Systems and Computers, 1998) states the soundness theorem, and van der Aalst and van Hee’s Workflow Management: Models, Methods, and Systems (MIT Press, 2002) develops the engineering around it.