Workflow Net (WF-net)

A subclass of Petri nets specifically designed to model business-process control flow. Introduced by van der Aalst (1997) as the formal substrate over which workflow correctness can be reasoned about.

Definition

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

PN has two distinguished places: a source i with •i = ∅ (no incoming arcs) and a sink o with o• = ∅ (no outgoing arcs).
Adding a fresh transition t* with •t = {o} and t*• = {i} yields a strongly connected Petri net.

Constraint (2) ensures the absence of dangling tasks/conditions — every place and transition lies on some path from i to o.

Intuition

A case is the unit of work (one customer order, one insurance claim, ...).
The case enters the procedure at the moment a token is placed in i.
The case is completed when a token appears in o (and all other places are empty — see concepts/soundness for the formal completion criterion).
Tasks are modelled as transitions; causal precedence between tasks is encoded by places connecting them.

Subclasses

The 1997 paper distinguishes three nested classes (each weaker decidability bound):

Class	Definition	Soundness decidability
WF-net	as above	EXPSPACE-hard via coverability graph
Free-choice WF-net	for any places p₁, p₂: •p₁ ∩ •p₂ = ∅ ∨ •p₁ = •p₂ — choice and synchronisation are separated	Polynomial time (Desel & Esparza Rank theorem)
Almost free-choice WF-net	free-choice + zero-or-more "inquiry" transitions that don't change net state	Polynomial time (reduce to free-choice)

In practice, the WF-nets supported by typical WFMSs (and corresponding BPMN-style models with AND/XOR splits/joins) are free-choice — the choice of next task is local to a routing place, not entangled with parallel synchronisation.

What WF-nets do not capture (in this paper)

Resources / actors — abstracted away; resources are listed in §3.1 as the second dimension of a workflow specification but the paper deliberately abstracts from them.
Case data — modelled as non-deterministic choice; data-conditional routing not formalised here.
Time — no timer constructs.
Compensation, exceptions — basic class only.

These dimensions are addressed in later work (CPNs for time, Data-Aware WF-nets for data, etc.) and in richer notations like BPMN.

Relationship to BPMN

A BPMN process model with one start event, one end event, and AND/XOR gateways can be mechanically translated into a WF-net, with:

BPMN tasks → Petri-net transitions
BPMN sequence flows ↔ Petri-net places (via routing transitions for AND/XOR splits/joins)

The translation is direct for free-choice cases; OR-gateways pose semantic challenges (cf. concepts/7pmg G5: "Avoid OR routing elements") and may not yield free-choice nets.

Soundness of the WF-net then implies a corresponding correctness property of the BPMN model.

Why WF-nets matter

They give a formal semantics to control-flow modelling, independent of any specific notation (BPMN, EPC, YAWL all map to WF-nets or extensions).
They make correctness a decidable property (concepts/soundness).
They support constructive design via soundness-preserving transformation rules.
They underpin process mining algorithms — discovered models are often expressed as WF-nets (sources/2011-vanderaalst-process-mining-book) and conformance is measured against WF-net behaviour.

Tool ecosystem

WOFLAN (original verifier).
ProM (analysis suite — discovery, conformance, performance — over Petri-net / WF-net models).
CPN Tools (for Coloured Petri Nets — extension of WF-nets with data and time).

concepts/soundness (the property WF-nets are designed to support) · concepts/process-model-quality · concepts/conformance-checking · frameworks/bpmn (target notation that maps to WF-nets) · methods/process-mining-basics (mining produces WF-nets) · entities/wil-van-der-aalst

Source

sources/1998-vanderaalst-verification-of-workflow-nets