---
title: Livelock (Process Model Behavioural Anomaly)
type: concept
tags: [bpm, modelling, soundness, anomaly, behavioural-correctness, loops, verification]
sources:
  - "[[sources/2018-dumas-fundamentals-of-bpm]]"
  - "[[sources/2018-dumas-fundamentals-of-bpm-ch5-discovery]]"
  - "[[sources/1998-vanderaalst-verification-of-workflow-nets]]"
created: 2026-05-04
updated: 2026-05-04
---

# Livelock

A **behavioural anomaly** in which a token is trapped within a loop structure: it can move (unlike a deadlocked token) but only inside the loop, never reaching an end event.

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

> *A livelock is another type of behavioural anomaly which occurs when a process instance keeps cycling within a loop. In other words, a token is trapped within a loop structure: it is free to move but only within the loop.*

## How livelocks arise in BPMN

| Pattern | Why it livelocks |
|---|---|
| **Loop with always-true exit-true condition routing back** | Exit condition guards inverted — token always loops |
| **Loop with always-false exit condition** | Token can never exit the loop |
| **Cycle with no exit gateway at all** | Modeller forgot to add the exit branch |
| **Infinite multi-instance with no completion condition** | Multi-instance loop with unspecified or unsatisfiable completion criterion |

A livelocked instance, like a deadlocked one, **violates option to complete** ([[concepts/soundness]] clause 1) — the instance never reaches an end event.

## Distinction from deadlock

| | Deadlock | Livelock |
|---|---|---|
| Token state | Stuck — cannot move | Active — moves continuously |
| Visible symptom | Process appears frozen | Process appears busy but makes no progress |
| Cause | Missing synchronisation token (e.g., AND-join wait) | Loop-exit condition unsatisfiable or wrong-polarity |
| Detection by inspection | Easier — gateway mismatch usually obvious | Harder — requires reasoning about loop conditions |

## Detection

- **Reachability analysis**: a livelocked state is one where the model has no path to any end event from the current marking, even though transitions are still firable. Same liveness check that catches deadlocks ([[sources/1998-vanderaalst-verification-of-workflow-nets]] Theorem 11).
- **Token simulation**: simulate cases through the model; livelocks manifest as instances that loop indefinitely without producing an end-event token.
- **Code review of loop conditions**: every loop must have an exit condition that *can* evaluate true; the modelled state must be able to *cause* the condition to become true.

## Prevention

- **Bound every loop** with an explicit exit condition that becomes true when the work is done. The condition must reference state that the loop body can actually change.
- **Use boundary timer events** for "give up after N iterations / time" patterns.
- **Multi-instance constructs** (parallel ‖ or sequential ≡) over an explicit collection are safer than ad-hoc loops — completion is automatically tied to the collection size.
- For "redo on failure" patterns: add an explicit failure-counter or a timer-based escape.

## Example (Dumas Fig 5.12b)

A small cyclic model with a structurally-incorrect path (B is not on a path from start to end) plus a self-loop on the only routable activity. From the start event, executing the loop activity always returns to the same state — token cycles forever, never reaches the end event.

## Related
[[concepts/soundness]] · [[concepts/deadlock]] (sister anomaly) · [[concepts/lack-of-synchronization]] · [[concepts/dead-activity]] · [[concepts/workflow-net]] · [[concepts/block-structure]] · [[frameworks/bpmn]]

## Sources
[[sources/2018-dumas-fundamentals-of-bpm]] §5.4.1 · [[sources/2018-dumas-fundamentals-of-bpm-ch5-discovery]] · [[sources/1998-vanderaalst-verification-of-workflow-nets]]