Coloured Petri Net¶

A Petri-net formalism whose tokens carry typed data values called colours and whose transitions use variables, guards, and arc expressions, compactly representing families of similar concurrent states and events.

Version: v1 · 2026-09-28 · History
Domain-specific #: 8555
Domain group: Applied Sciences & Engineering
Origin domain: Computer Science & Software Engineering
Subdomains: Formal Models of Concurrency, Petri Nets → Computer Science & Software Engineering
Aliases: Colored Petri Net, CPN, Coloured Petri Nets

Core Idea¶

A coloured Petri net adds data to the token game of a Petri net. Places still contain markings and transitions still consume and produce tokens, but variables, types, guards, and expressions let one graph describe many value-specific cases.

The gain is compact, executable concurrency modeling; the cost is a richer state space and formalism-dependent semantics. Analysis must name the CPN dialect, property, state abstraction, and any unfolding or reduction.

How would you explain it like I'm…

Board Game with Labeled Tokens

Think of a board game where tokens move between circles along arrows. In a plain version, all tokens look the same. In a Coloured Petri Net, each token carries a little label, like a number or a name, and the rules for moving can check those labels. That way one small board can describe lots of different situations.

Petri Net Tokens with Data

A Petri net is a kind of diagram for showing things happening at the same time. It has places that hold tokens and transitions that take tokens from some places and put new ones in others. A Coloured Petri Net adds data to the tokens, so each token carries a value, like a customer number. Transitions can have rules, called guards, that check those values, and expressions that decide what values the new tokens get. This lets one small diagram stand for many cases at once, and you can even run it like a program, but checking it is harder because there are many more possible states.

Data-Carrying Petri Nets

A Coloured Petri Net (CPN) extends an ordinary Petri net by attaching data values to tokens. As in a regular Petri net, places hold markings, meaning collections of tokens, and transitions fire by consuming tokens from input places and producing tokens in output places. In a CPN, tokens have types, and arcs and transitions use variables, guards, which are conditions a transition must satisfy, and expressions that compute the values of produced tokens. This lets a single graph describe many value-specific cases compactly and be executed as a model of concurrent behavior. The trade-off is a much larger state space and semantics that depend on the specific CPN formalism. Any analysis should state which CPN dialect, which property is checked, how states are abstracted, and whether the net was unfolded or reduced.

A Coloured Petri Net adds typed data to the token game of Petri nets. Places carry markings, and transitions consume and produce tokens, but tokens are typed values, arcs carry expressions over variables, and transitions carry guards restricting the variable bindings under which they may fire. One net thereby folds together many value-specific instances of the same structure, giving compact, executable models of concurrent systems. The price is a richer state space, since markings range over data values, and semantics that depend on the chosen formalism. Rigorous analysis must name the CPN dialect, the property being verified, the state abstraction used, and any unfolding to an ordinary Petri net or reduction applied. Without those, claims about CPN behavior are underdetermined.

Structural Signature¶

Sig role-phrases:

Places — Hold multisets of typed coloured tokens. It is state locations. Counterfactual: Each place's colour set limits values.
Transitions — Represent event schemas that may fire under a binding. It is events. Counterfactual: One transition can stand for many value instances.
Colour sets — Define token data types and available operations. It is type system. Counterfactual: Colour is data, not necessarily a visual hue.
Arc expressions — Select, consume, and produce token values around transitions. It is flow rules. Counterfactual: Expressions must type-check against connected places.
Guards and variable bindings — Restrict which transition instances are enabled. It is enabling logic. Counterfactual: Concurrency depends on competing token bindings.
Marking and initialization — Specify the current and initial multisets of coloured tokens. It is state. Counterfactual: State identity includes both location and value multiplicity.

What It Is Not¶

It is not graph colouring.
Token colour is a typed value, not merely a drawing colour.
It is not automatically timed or stochastic.
A workflow diagram without Petri firing semantics is not a CPN.
Closest near-miss. An ordinary Petri net treats tokens at a place as indistinguishable; a coloured Petri net distinguishes typed values and can unfold value instances into a larger ordinary net under suitable finite conditions.

Scope of Application¶

Concurrent software. Models processes, messages, resources, and synchronization.
Communication protocols. Represents typed packets and value-dependent transitions.
Business and manufacturing systems. Models cases, jobs, machines, and routing.
Formal verification. Supports simulation, reachability, invariant, and state-space analysis.

Clarity¶

State CPN formalism/tool/version, places and transitions, colour sets and type definitions, variables, arc expressions and multiplicities, guards, initial marking, firing and binding semantics, concurrency and conflict, hierarchy, time or probability extensions, finite/infinite colours, unfolding relation, state-space method and reductions, fairness, properties/invariants, simulation parameters, validation against the real system, and whether visual token hues have semantic meaning.

Manages Complexity¶

One graphical transition can denote many bindings, and token values interact with multiplicity, concurrency, hierarchy, and expression evaluation. Compact models can conceal enormous or infinite state spaces.

Abstract Reasoning¶

Define system entities as colour sets and state locations as typed places.
Specify transition variables, guards, and arc expressions with type checking.
Construct the initial coloured marking and precise firing semantics.
Simulate diagnostic traces and validate model behavior against requirements.
Choose symbolic, unfolded, invariant, or reduced analysis appropriate to the property and colour domains.

Knowledge Transfer¶

Typed-token concurrency reasoning transfers to high-level Petri nets, workflow languages, and actor protocols when their execution semantics are mapped explicitly. CPN verification results and tool syntax should not be transferred across dialects or infinite colour sets without revalidation.

Examples¶

Canonical¶

A protocol model gives each packet token a record colour containing sender, receiver, and sequence number; a transmit transition binds one packet, checks a route guard, consumes it from a queue place, and produces a transformed token in the channel place.

Mapped back: tokens → packet records; places → typed queues; transition → transmit schema; guard → route condition; arcs → consume and transform binding.

Applied / In Practice¶

An ordinary Petri-net diagram draws some tokens red and blue only to help the viewer, but firing ignores the colours. Visual decoration without typed value semantics is not a coloured Petri net.

Mapped back: appearance → different hues; semantics → tokens indistinguishable; verdict → ordinary Petri net.

Structural Tensions¶

T1 — Model Compactness versus Analysis Expansion. Colours collapse repeated structures while unfolding or symbolic state exploration can still produce a very large state space.

Diagnostic: Which representation and reduction support the target property?

T2 — Expressive Data versus Formal Tractability. Rich types and expressions model realistic systems while complicating reachability, equivalence, and tool interoperability.

Diagnostic: What minimal colour language is sufficient?

Structural–Framed Character¶

Coloured Petri Net is structural as Petri-net concurrency parameterized by typed token values and framed by guards, expressions, and bindings.

Structural Core vs. Domain Accent¶

The broad pattern is a state-transition model. CPNs add token data types, multiset markings, variable bindings, guard predicates, arc expressions, compact symmetry, and a tradeoff between visual compression and state-space growth.

This entry is a kind of Petri net.

Approved formal-model root. No frozen parent entails typed-token Petri firing semantics.
Related — Petri net, high-level Petri net, predicate/transition net, stochastic Petri net, timed Petri net, token, marking, reachability, CPN Tools, and unfolding. They are base formalism, family, variants, components, analysis, tool, and translation.

Relationships to Other Abstractions¶

Current abstraction Coloured Petri Net Domain-specific

Parents (1) — more general patterns this builds on

Coloured Petri Net is a kind of Petri net Domain-specific

Coloured Petri Net is a domain-specific kind of petri net under its frozen identity and differentia. Complete-catalog comparison found the corresponding live broader identity.

Hierarchy path (1) — routes to 1 parentless root

Coloured Petri Net → Petri net → Network → Reservoir-Flux Network → Conservation Laws → Invariance

Neighborhood in Abstraction Space¶

Coloured Petri Net sits in a moderately populated region (50^th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.

Family — Formal Systems & Discrete Structures (18 abstractions)

Nearest neighbors

Generalized Büchi Automaton — 0.87
Loop (Graph Theory) — 0.86
Intersection Non-Emptiness Problem — 0.86
Cyclic Category — 0.86
Mapping Cylinder — 0.85

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With¶

Graph colouring. Tell: Assigns colours to vertices or edges under adjacency constraints.
Ordinary Petri net. Tell: Uses indistinguishable tokens at each place.
Stochastic Petri net. Tell: Adds probabilistic timing and need not use token colours.
Finite-state machine. Tell: Has single-state transition semantics rather than distributed multiset markings.

References¶

Frozen Wikipedia discovery revision: https://en.wikipedia.org/wiki/Coloured_Petri_net (revision 1041112706).
Preserved source candidate: https://archive.org/details/springer_10.1007-978-3-642-60794-3
Preserved source candidate: https://archive.org/details/springer_10.1007-978-3-642-60794-3/page/n236

The frozen Wikipedia revision is discovery provenance. The retained source set was reviewed for identity, formal or operational relation, and scope. The encyclopedia's structural synthesis is bounded to those claims; a thin authority surface is recorded as a nonblocking source-strengthening repair rather than concealed.