Verification of Workflow Nets

Foundational paper formalising workflow soundness as a Petri-net-theoretic property and reducing it to liveness and boundedness — making the correctness of business processes decidable, and for an important subclass, decidable in polynomial time. Cited by virtually every BPM-verification paper since 1997.

Petri-net preliminaries (§2)

Standard apparatus the paper rests on:

Petri net = (P, T, F) where P (places), T (transitions), F ⊆ (P×T) ∪ (T×P) (flow relation, weight 1 in workflow context).
State / marking M: P → ℕ (token distribution).
Firing rule: transition t enabled iff every input place has ≥1 token; firing consumes 1 from each input, produces 1 to each output.
Reachability M₁ →* Mₙ via firing sequences.
Live: from every reachable state, every transition can be enabled in some future state.
Bounded: token count in every place stays bounded across all reachable states.
Strongly connected: for every pair of nodes x, y, a directed path leads from x to y.
Free-choice (Def 5): for any two places p₁, p₂, either •p₁ ∩ •p₂ = ∅ or •p₁ = •p₂ (where •p is the set of transitions sharing p as an input). Choice is "made inside an OR-split", not entangled with parallelism.

Workflow Net definition (§3.3, Def 6)

A Petri net PN = (P, T, F) is a WF-net iff:

PN has two special places: input i with •i = ∅ (source) and output o with o• = ∅ (sink).
Adding a fresh transition t* with •t = {o}, t*• = {i} yields a strongly connected net.

Constraint (2) prevents dangling tasks/conditions that cannot contribute to case processing.

The Soundness Property (§3.4, Def 7)

A WF-net PN is sound iff:

Option to complete: ∀M (i →* M) ⇒ (M →* o) — from any reachable state, the final state o can be reached.
Proper completion: ∀M ((i →* M) ∧ (M ≥ o)) ⇒ (M = o) — when a token reaches o, all other places are empty (no orphan tokens).
No dead transitions: ∀t∈T ∃M, M' (i →* M →ᵗ M') — every transition is executable from some reachable state.

Sometimes (i)+(ii) together are called proper termination; (iii) is no dead activities. Lazcoz/de Hert and Dumas et al. textbooks cite this triple verbatim.

A common informal formulation in the paper introduces the property pre-formally:

For any case, the procedure will terminate eventually, and at the moment the procedure terminates there is a token in place o and all the other places are empty.

The fairness assumption (any infinitely-often-enabled transition fires eventually) is reasonable in workflow contexts and lets (i) imply eventual termination.

Verification reduction (§4.2, Theorem 11)

Define PN-bar by adding t* to PN connecting o back to i. Then:

Theorem 11: WF-net PN is sound ⇔ (PN-bar, i) is live and bounded.

This is the load-bearing result of the paper: it reduces a workflow-specific correctness property to two well-studied Petri-net properties, making any standard liveness/boundedness analysis tool applicable to workflow verification.

Polynomial-time decidability (§4.3, Theorems 12–16)

For arbitrary WF-nets, even though Theorem 11 reduces soundness to standard Petri-net properties, those problems are EXPSPACE-hard in the general case.

For free-choice WF-nets:

Theorem 12: Soundness decidable in polynomial time (consequence of the Rank theorem on free-choice nets, Desel & Esparza 1995).
Theorem 14: Sufficient condition — rank(PN-bar) = clusters − 1 ∧ every proper siphon contains at least one token — checkable in polynomial time.

For almost free-choice WF-nets (free-choice + zero-or-more inquiry transitions that don't change net state):

Theorem 16: Soundness decidable in polynomial time by reducing to free-choice via inquiry-transition removal.

The author reports that almost free-choice covers the WF-nets actually encountered in industry projects (Dutch Customs, Dutch Justice, banks, insurance).

Soundness-preserving transformations (§5)

Eight basic transformation rules (Figs 7–10) enable safe modification of running workflows:

Rule	Effect	Inverse
T1a	Division: replace task t₁ with two consecutive tasks t₂, t₃	T1b (aggregation)
T2a	Specialisation: replace t₁ with two conditional tasks t₂, t₃	T2b (generalisation)
T3a	Parallelisation: replace t₁ with two parallel tasks t₂, t₃ (with fork/join)	T3b
T4a	Iteration: replace t₁ with iteration of t₂	T4b

Composites: T5a (replace two consecutive tasks with two parallel tasks), T5b (inverse).

Theorem 18: Each rule preserves soundness — applying any rule to a sound WF-net yields a sound WF-net. Proof relies on preserving liveness and boundedness of the extended net.

Corollary 19: Any WF-net constructed from the trivial single-task WF-net by applying a sequence of these rules is sound by construction — a constructive counterpart to verification.

The converse is false: there exist sound WF-nets not constructible by these rules (e.g., the inquiry-augmented WF-net of Fig 6). The rules cover the routing primitives of typical WFMSs but are not complete for the full sound class.

Tool: WOFLAN

WOrkFlow ANalyser — Petri-net-based analysis tool implementing the verification techniques. Many later BPM-verification tools (ProM-based and others) descend from this lineage.

Significance

This paper establishes:

What "correctness" means for a workflow (Definition 7) — beyond mere syntactic well-formedness.
That correctness is decidable, and tractable for the practical subclass (Theorem 12).
A constructive framework for change management of running processes (transformation rules + Corollary 19).

It is the formal foundation underneath the lay phrasings ("option to complete", "proper completion", "no dead activities") that appear in sources/2018-dumas-fundamentals-of-bpm §5.4 and downstream BPM textbooks.

Connections

Concepts: concepts/soundness · concepts/workflow-net · concepts/process-model-quality (the syntactic/structural pillar) Sources: sources/2018-dumas-fundamentals-of-bpm (textbook citation) · sources/2010-mendling-reijers-vanderaalst-7pmg (G3 motivated partly by enabling soundness) · sources/2011-vanderaalst-process-mining-book (van der Aalst's later monograph builds on this lineage) Author / hub entity: entities/wil-van-der-aalst

Open follow-ups

Resource-aware soundness extensions (Aalst flags this in §7).
Weak / relaxed / lazy soundness variants (introduced in subsequent papers — not in this one; candidates for future ingest).
Data-aware soundness (later work, Sidorova et al.; Trcka et al.).