Est. 1979 Advanced

High-Level Petri Nets

A family of formal graphical modelling languages that extend classical Petri nets with typed data, enabling concise specification of concurrent and distributed systems.

Created by Hartmann J. Genrich, Kurt Lautenbach, Kurt Jensen (and others)

Paradigm Formal specification, Graphical modelling, Concurrent
Typing Static, Strong (typed tokens via colour sets)
First Appeared 1979
Latest Version ISO/IEC 15909-1:2019 (revised standard)

Overview

High-Level Petri Nets (HLPN) are a family of formal, graphical modelling languages that extend the classical Petri nets introduced by Carl Adam Petri in 1962. Where classical (place/transition) Petri nets use indistinguishable “black” tokens, high-level Petri nets attach structured data to tokens and use expressions on arcs and transitions, dramatically compacting models of complex concurrent and distributed systems.

The umbrella term “high-level Petri nets” covers several closely related formalisms, the most prominent being Predicate/Transition Nets (PrT-nets) developed by Hartmann J. Genrich and Kurt Lautenbach, and Coloured Petri Nets (CP-nets or CPN) developed by Kurt Jensen. These were later unified under the international standard ISO/IEC 15909, which provides a common mathematical definition and a graphical notation.

High-level Petri nets are not a general-purpose programming language in the conventional sense. They are a formal specification and modelling language: models are typically built in a graphical editor, executed via simulation, and analysed by techniques such as state-space exploration, invariant analysis, and model checking.

History & Origins

Petri nets were introduced in Carl Adam Petri’s 1962 dissertation Kommunikation mit Automaten at the University of Bonn. The basic formalism is elegant but quickly becomes unwieldy for real systems, because every distinct value or process instance must be encoded as a separate place or token configuration. By the late 1970s, researchers were exploring ways to combine the concurrency semantics of Petri nets with the expressive power of higher-level data types and predicate logic.

Two parallel strands of work shaped the field:

  • Predicate/Transition Nets were introduced by Hartmann J. Genrich and Kurt Lautenbach at GMD (the German National Research Center for Information Technology) in a foundational 1979 paper. In PrT-nets, tokens are structured individuals (tuples), and transitions are guarded by predicates over the variables that bind to incoming tokens.
  • Coloured Petri Nets were introduced by Kurt Jensen at Aarhus University in 1981. CP-nets associate a colour set (a data type) with each place, and arc expressions describe how tokens of those types flow through transitions. Jensen’s later three-volume monograph (Springer, 1992–1997) became the standard reference.

Other related high-level formalisms include Coloured Petri Nets with hierarchies, Algebraic Petri Nets, and Object-Oriented Petri Nets, all of which share the core idea of enriching tokens with structure.

Design Philosophy

High-level Petri nets are designed around a small set of guiding ideas:

  • Make concurrency first-class. The graphical structure of a net directly expresses which events may occur independently and which must synchronise, without hiding concurrency inside an interleaving semantics.
  • Combine data and control. Classical Petri nets describe pure control flow; high-level Petri nets layer typed data on top, so that a single transition can describe a parameterised family of events.
  • Stay mathematically grounded. Every well-formed high-level net has a precise formal semantics, enabling analysis techniques such as reachability analysis, place/transition invariants, and model checking against temporal logics.
  • Support graphical reasoning. Models are drawn as bipartite graphs of places (circles) and transitions (rectangles) connected by arcs, with the intent that humans can read and reason about a model visually as well as formally.

Key Features

A typical high-level Petri net (in the style of CP-nets and ISO/IEC 15909) provides:

  • Places typed by colour sets (data types), holding multisets of typed tokens.
  • Transitions annotated with guard expressions that restrict when they may fire.
  • Arc expressions describing the multisets of tokens consumed from input places and produced on output places when a transition fires.
  • Variables that are bound by the tokens consumed on input arcs and reused in guards and output arc expressions.
  • Hierarchies and substitution transitions (in hierarchical CP-nets) that allow large models to be decomposed into reusable modules.
  • Time and stochastic extensions in several dialects (Timed CP-nets, Stochastic Petri Nets) for performance analysis.

The mathematical semantics is given in terms of enabled bindings and step sequences: a transition is enabled for a particular binding of its variables when the multiset described by its input arc expressions is present on its input places and its guard evaluates to true.

Standardisation

High-level Petri nets are one of the relatively few graphical modelling languages with an ISO standard:

  • ISO/IEC 15909-1 defines the concepts, definitions, and graphical notation for high-level Petri nets. The first edition was published in 2004 and a revised edition in 2019.
  • ISO/IEC 15909-2 defines the Petri Net Markup Language (PNML), an XML-based transfer format that allows different tools to exchange Petri net models. It was first published in 2011.
  • ISO/IEC 15909-3 addresses extensions and structuring mechanisms for high-level Petri nets.

The standard is intentionally tool-agnostic: it specifies the formalism rather than mandating any particular implementation.

Tooling

Several tools implement high-level Petri net formalisms; the best-known include:

  • CPN Tools, originally developed by the CPN Group at Aarhus University, providing graphical editing, simulation, and state-space analysis of Coloured Petri Nets with inscriptions written in CPN ML (a dialect of Standard ML).
  • Snoopy and Charlie, developed at the Brandenburg University of Technology Cottbus, for modelling and analysis of various Petri net classes including coloured and stochastic variants.
  • TINA (TIme petri Net Analyzer), developed at LAAS-CNRS, supporting time Petri nets and related analyses.
  • GreatSPN, developed at the University of Turin, for stochastic and generalised stochastic Petri nets.

Many of these tools support PNML import/export, making it possible to move models between environments.

Current Relevance

High-level Petri nets remain an active topic in academic research, particularly in the communities around the annual International Conference on Application and Theory of Petri Nets and Concurrency, which has been held since 1980, and the Springer LNCS journal Transactions on Petri Nets and Other Models of Concurrency (ToPNoC). They are widely taught in graduate courses on concurrency theory, formal methods, and model-based systems engineering.

In industry, high-level Petri nets are less ubiquitous than UML or BPMN, but their formal semantics make them attractive in domains where rigorous analysis matters: communication protocols, workflow verification, manufacturing control, embedded systems, and safety-critical software. Petri net concepts also continue to influence neighbouring fields, including business process modelling (notably through Wil van der Aalst’s work on workflow nets and process mining) and discrete-event simulation.

Why It Matters

High-level Petri nets occupy a distinctive niche: they are graphical, formal, executable, and concurrent by design. They demonstrated that a visual modelling language can have a rigorous mathematical semantics without sacrificing expressiveness, and they provided one of the earliest, most enduring frameworks for reasoning about concurrent systems at a level that is both abstract enough to be tractable and concrete enough to be analysed.

For students of programming languages and formal methods, high-level Petri nets are a reminder that “language” is broader than text on a screen — and that some of the most influential ideas about concurrency, data flow, and verification arrived not as keywords in a compiler, but as circles, rectangles, and arrows on a diagram.

Timeline

1962
Carl Adam Petri publishes his doctoral dissertation 'Kommunikation mit Automaten' at the University of Bonn, founding the theory of (classical) Petri nets.
1979
Hartmann J. Genrich and Kurt Lautenbach publish the foundational paper on Predicate/Transition Nets, one of the first high-level Petri net formalisms, generalising tokens to structured individuals.
1981
Kurt Jensen introduces Coloured Petri Nets (CP-nets) at Aarhus University, attaching typed 'colours' to tokens and arc expressions.
1992
Volume 1 of Kurt Jensen's monograph 'Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use' is published by Springer.
2003
CPN Tools is released by the CPN Group at Aarhus University, providing graphical editing, simulation, and state-space analysis of Coloured Petri Nets.
2004
ISO/IEC 15909-1:2004 'High-level Petri nets - Part 1: Concepts, definitions and graphical notation' is published, providing an international standard for the formalism.
2011
ISO/IEC 15909-2:2011 is published, defining the Petri Net Markup Language (PNML) as a standard transfer format for high-level Petri nets.
2019
ISO/IEC 15909-1:2019 is published as a revised edition of the high-level Petri nets standard.

Notable Uses & Legacy

Aarhus University CPN Group

Developed and maintains CPN Tools, the reference modelling and analysis environment for Coloured Petri Nets, used in research and teaching of concurrent systems.

Telecommunications protocol modelling

Coloured Petri Nets have been used in academic and industrial case studies to model and verify communication protocols, including studies published in the Springer LNCS Transactions on Petri Nets and Other Models of Concurrency.

Workflow and business process modelling

Wil van der Aalst's work on workflow nets builds on Petri net theory and influenced the formal semantics of business process modelling tools used in workflow management research.

Embedded and control systems research

High-level Petri nets are applied in academic literature for modelling discrete-event control systems, manufacturing systems, and embedded controllers where concurrency and synchronisation are central.

Petri Nets conference community

The annual International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets) has run since 1980, with high-level Petri nets as a recurring topic in its proceedings (Springer LNCS).

Language Influence

Influenced By

Petri Nets

Influenced

Coloured Petri Nets CPN ML

Running Today

Run examples using the official Docker image:

docker pull
Last updated: