---
title: "Verification of Workflow Nets"
type: source
tags: [bpm, petri-nets, workflow-nets, soundness, verification, formal-methods, free-choice]
authors: [van der Aalst, Wil M.P.]
year: 1998
venue: "Application and Theory of Petri Nets 1997 (ATPN'97), LNCS 1248, Springer-Verlag, pp. 407–426"
kind: paper
raw_path: "raw/Process Frameworks & BPM/1998-vanderaalst-verification-of-workflow-nets.pdf"
sources: []
key_claims:
  - "Workflow Nets (WF-nets) are a subclass of Petri nets with two distinguished places — source i and sink o — such that adding a transition t* connecting o back to i yields a strongly connected net (Definition 6)."
  - "A WF-net is sound (Definition 7) iff: (i) every reachable state can reach the final state with one token in o (option to complete); (ii) the final state with one token in o is the only reachable state with ≥1 token in o (proper completion); (iii) there are no dead transitions in (PN, i) (every task is executable from some reachable state)."
  - "Theorem 11: A WF-net PN is sound if and only if (PN-bar, i) — the net extended with t* connecting o→i — is live and bounded. Soundness reduces to standard Petri-net liveness/boundedness analysis."
  - "Theorem 12: For free-choice WF-nets, soundness is decidable in polynomial time (via Rank theorem from Desel & Esparza)."
  - "Theorem 14: A WF-net PN is sound if rank(PN-bar) equals (clusters − 1) and every proper siphon contains at least one token — sufficient condition checkable in polynomial time without full state-space exploration."
  - "Almost free-choice WF-nets — free-choice extended with inquiry transitions — preserve polynomial-time decidability for soundness (Theorem 16)."
  - "Eight basic transformation rules (T1a/b division/aggregation, T2a/b specialisation/generalisation, T3a/b parallelisation, T4a/b iteration) plus composite rules T5a/b preserve soundness — Theorem 18. Useful for safe modification of running workflows."
  - "Coverability-graph brute-force soundness checking is at best EXPSPACE-hard; the live-and-bounded reduction + free-choice restriction is what makes WF-net verification tractable in practice."
  - "Most WFMS-supported workflows are (almost) free-choice in practice — the OR-split building block is naturally free-choice; OR-joins outside this class are rare in the tools the author surveyed."
  - "WOFLAN (WOrkFlow ANalyser) implements the verification techniques described in this paper."
created: 2026-05-04
updated: 2026-05-04
---

# 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:
1. PN has two special places: input *i* with •*i* = ∅ (source) and output *o* with *o*• = ∅ (sink).
2. 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:

1. **Option to complete**: ∀M (i →* M) ⇒ (M →* o) — from any reachable state, the final state *o* can be reached.
2. **Proper completion**: ∀M ((i →* M) ∧ (M ≥ o)) ⇒ (M = o) — when a token reaches *o*, all other places are empty (no orphan tokens).
3. **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:
1. **What "correctness" means for a workflow** (Definition 7) — beyond mere syntactic well-formedness.
2. **That correctness is decidable, and tractable for the practical subclass** (Theorem 12).
3. **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.).