Deadlock

A behavioural anomaly in which a running process instance reaches a state from which it cannot progress further. A token gets stuck. The instance can never complete.

Definition (sources/2018-dumas-fundamentals-of-bpm §5.4.1):

A deadlock occurs when a running process instance is not able to progress any further once a given state is reached, i.e., a token gets stuck at that state.

How deadlocks arise in BPMN

The most common cause is a mismatched split-join pair:

Pattern	Why it deadlocks
XOR-split → AND-join	XOR routes a token down one branch only; the AND-join waits for tokens on all incoming branches → wait forever
OR-split (incomplete coverage) → AND-join	If conditions don't activate all branches the AND-join expects, the same wait-forever
Branch injected into AND-block	Token returning from the injection arrives at the AND-join but the symmetrically-expected token never appears (Fig 5.12a)
Loop with always-false exit + AND-join entry	Internal AND-join in a loop body never gets the second token

A model with a deadlock violates option to complete (the first soundness clause — see concepts/soundness).

Detection

Mechanical: any standard Petri-net liveness checker flags deadlocks. See sources/1998-vanderaalst-verification-of-workflow-nets Theorem 11 — soundness reduces to live + bounded on the extended net; deadlocks violate liveness.

Practical tools:

WOFLAN (workflow-specific verifier).
ProM (process-mining suite, multiple soundness plug-ins).
Camunda Modeler (basic structural validation; not full deadlock detection).
bpmn-js-token-simulation — visual token-flow simulator; deadlocks become observable as stuck tokens.

By inspection: walk every gateway and check that for every split there is a matching join of the same type. This catches most deadlocks at design time.

Prevention

Three modes (cf. concepts/soundness §"achieving correctness"):

Verification after the fact — build, then check.
Construction by design — use a tool that prevents soundness-violating edits.
Block-structuring — every split paired with a same-type join; sound by construction.

concepts/7pmg G3 (single start/end) and G4 (model as structured) reduce deadlock incidence empirically.

Example (Dumas Fig 5.12a)

A model with an apparent AND-block has an extra branch injected such that activity G's path bypasses one half of the AND-block. If G is executed, a token arrives at the AND-join — but the AND-join expects two tokens (one from each branch of the original block). The second token never arrives → deadlock.

Anomaly	Symptom
Deadlock	Token unable to progress; instance never completes
concepts/livelock	Token cycles in a loop forever; instance never completes
concepts/lack-of-synchronization	Multiple tokens on same flow; instance "completes" with extra tokens
concepts/dead-activity	Activity never executable in any instance

Deadlocks and livelocks both violate option to complete but for different reasons — stuck vs. spinning.

concepts/soundness · concepts/workflow-net · concepts/block-structure · concepts/livelock · concepts/lack-of-synchronization · concepts/dead-activity · concepts/process-model-quality · concepts/7pmg · frameworks/bpmn

Sources

sources/2018-dumas-fundamentals-of-bpm §5.4.1 (textbook treatment) · sources/2018-dumas-fundamentals-of-bpm-ch5-discovery · sources/1998-vanderaalst-verification-of-workflow-nets (formal Petri-net foundation)