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

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.

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. Inclusion test: Require Petri-net places, transitions, markings, and firing semantics extended with typed token values and value-dependent expressions or guards under a defined coloured-net formalism. Exclusion test: Exclude graph colouring, tokens drawn in different display colours with no data semantics, ordinary place/transition nets, stochastic or timed Petri nets unless colour semantics are also present, finite-state machines, business-process diagrams without token firing semantics, and any typed transition system automatically labeled a CPN. Nearest boundary: 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. Exit condition: Meaning changes with CPN dialect and tool, colour-set finiteness, expression language, variables and binding rules, guard semantics, arc multiplicities, inhibitor/reset extensions, timing or stochastic annotations, hierarchy, initialization, fairness, unfolding, state-space reduction, and property checked. Common misclassifications: 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. Nearest named distinctions: Graph colouring: Assigns colours to vertices or edges under adjacency constraints. Ordinary Petri net: Uses indistinguishable tokens at each place. Stochastic Petri net: Adds probabilistic timing and need not use token colours. Finite-state machine: Has single-state transition semantics rather than distributed multiset markings.

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

1. Define system entities as colour sets and state locations as typed places.
2. Specify transition variables, guards, and arc expressions with type checking.
3. Construct the initial coloured marking and precise firing semantics.
4. Simulate diagnostic traces and validate model behavior against requirements.
5. 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.

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