---
title: Workflow Net (WF-net)
type: concept
tags: [bpm, petri-nets, formal-methods, modelling, control-flow]
sources:
  - "[[sources/1998-vanderaalst-verification-of-workflow-nets]]"
created: 2026-05-04
updated: 2026-05-04
---

# 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:

1. PN has two distinguished places: a **source** *i* with •*i* = ∅ (no incoming arcs) and a **sink** *o* with *o*• = ∅ (no outgoing arcs).
2. 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.

[[concepts/soundness|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).

## Related
[[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]]