ISO/IEC 15909-1:2019

Systems and software engineering - High-level Petri nets - Part 1: Concepts, definitions and graphical notation

This document defines a Petri net modeling language or technique, called high-level Petri nets, including its syntax and semantics. It provides a reference definition that can be used both within and between organizations, to ensure a common understanding of the technique and of the specifications written using the technique. This document also facilitates the development and interoperability of Petri net computer support tools. This document is applicable to a wide variety of concurrent discrete event systems and in particular distributed systems. Generic fields of application include: - requirements analysis; - development of specifications, designs and test suites; - descriptions of existing systems prior to re-engineering; - modeling business and software processes; - providing the semantics for concurrent languages; - simulation of systems to increase confidence; - formal analysis of the behavior of systems; - and development of Petri net support tools. This document can be applied to the design of a broad range of systems and processes, including aerospace, air traffic control, avionics, banking, biological and chemical processes, business processes, communication protocols, computer hardware architectures, control systems, databases, defense command and control systems, distributed computing, electronic commerce, fault-tolerant systems, games, hospital procedures, information systems, Internet protocols and applications, legal processes, logistics, manufacturing systems, metabolic processes, music, nuclear power systems, operating systems, transport systems (including railway control), security systems, telecommunications and workflows.

Ingénierie du logiciel et des systèmes — Réseaux de Petri de haut niveau — Partie 1: Concepts, définitions et notation graphique

General Information

• Status: Published
• Publication Date: 26-Aug-2019
• ICS: 35.080 - Software
• Technical Committee: ISO/IEC JTC 1/SC 7 - Software and systems engineering
• Drafting Committee: ISO/IEC JTC 1/SC 7/WG 19 - Techniques for Specifying IT Systems
• Current Stage: 9093 - International Standard confirmed
• Start Date: 03-Jan-2025
• Completion Date: 30-Oct-2025

Relations

• Consolidated By: ISO 179-2:2020 - Plastics - Determination of Charpy impact properties - Part 2: Instrumented impact test
• Effective Date: 06-Jun-2022
• Revises: ISO/IEC 15909-1:2004 - Systems and software engineering - High-level Petri nets - Part 1: Concepts, definitions and graphical notation
• Effective Date: 16-Aug-2014
• Revises: ISO/IEC 15909-1:2004/Amd 1:2010 - Systems and software engineering - High-level Petri nets - Part 1: Concepts, definitions and graphical notation - Amendment 1: Symmetric Nets
• Effective Date: 16-Aug-2014

Overview - ISO/IEC 15909-1:2019 (High-level Petri nets)

ISO/IEC 15909-1:2019 defines high-level Petri nets as a standardized Petri net modeling language, including its syntax, semantics, execution semantics and graphical notation. Part 1 of the ISO/IEC 15909 series provides a formal semantic model and a mapping from graphical constructs to that model, enabling clear, unambiguous specifications and supporting tool interoperability. This second edition (2019) replaces the 2004 edition and reorganizes concepts in a simpler, modular way.

Keywords: ISO/IEC 15909-1, high-level Petri nets, Petri net modeling, graphical notation, semantics, concurrency, distributed systems.

Key Topics and Technical Requirements

• Semantic model and execution semantics: Precise mathematical definitions for nets, markings, enabling and firing rules so models are executable and analyzable.
• Net types covered: Place/Transition (P/T) nets, symmetric nets, high-level Petri nets, nets with priorities and time (time Petri nets). Conformance clauses specify mandatory and optional features.
• Conformance levels: Defines mandatory conformance items and levels (e.g., Level 1/Level 2, time and priority extensions) to ensure consistent interpretation across tools and organizations.
• Graphical notation and mapping: Standardized symbols and notational conventions plus rules to map graphical diagrams to the formal semantic model.
• Annex material: Includes normative mathematical conventions and informative guidelines for graphical notations to aid consistent modeling and implementation.
• Interoperability focus: Language and mapping intended to facilitate development of Petri net tools, model exchange and reproducible analyses.

Practical Applications and Who Uses This Standard

ISO/IEC 15909-1 is applicable to a wide variety of concurrent discrete-event and distributed systems. Typical uses include:

• Requirements analysis, specification and design of concurrent systems
• Modeling and simulation to validate behavior before implementation
• Formal analysis (liveness, reachability, deadlock) and test-suite development
• Re-engineering and documentation of existing systems
• Providing semantics for concurrent programming languages and communication protocols

Users who benefit most:

• Systems and software engineers, architects and modelers
• Tool developers and vendors building Petri net editors, simulators and analyzers
• Verification and QA teams in safety-critical domains (aerospace, avionics, nuclear, transport)
• Researchers and educators in formal methods and concurrent systems

Related Standards

• ISO/IEC 15909 series (other parts address model transfer formats and tool interoperability). Refer to national standards bodies or ISO for the complete list of parts and normative references.

ISO/IEC 15909-1:2019 provides the formal foundation and graphical conventions needed to model, analyze and exchange high-level Petri net specifications reliably across tools and organizations.

Standards Content (Sample)

INTERNATIONAL ISO/IEC
STANDARD 15909-1
Second edition
2019-08
Systems and software engineering —
High-level Petri nets —
Part 1:
Concepts, definitions and graphical
notation
Ingénierie du logiciel et des systèmes — Réseaux de Petri de haut
niveau —
Partie 1: Concepts, définitions et notation graphique
Reference number
©
ISO/IEC 2019
© ISO/IEC 2019
All rights reserved. Unless otherwise specified, or required in the context of its implementation, no part of this publication may
be reproduced or utilized otherwise in any form or by any means, electronic or mechanical, including photocopying, or posting
on the internet or an intranet, without prior written permission. Permission can be requested from either ISO at the address
below or ISO’s member body in the country of the requester.
ISO copyright office
CP 401 • Ch. de Blandonnet 8
CH-1214 Vernier, Geneva
Phone: [phone]
Fax: [phone]
Email: [e-mail]
Website: www.iso.org
Published in Switzerland
ii © ISO/IEC 2019 – All rights reserved

Contents Page
Foreword .v
Introduction .vi
1 Scope . 1
2 Normative references . 1
3 Terms and definitions . 1
4 Conformance . 5
4.1 General . 5
4.2 Mandatory conformance: common concepts for Petri nets . 5
4.3 Place/Transition nets . 5
4.4 Symmetric nets . 5
4.5 High-level Petri nets . 5
4.5.1 Level 1 . 5
4.5.2 Level 2 . 5
4.6 Petri nets with priorities . 5
4.7 Petri nets with time — Level 1 . 6
5 Common concepts for Petri nets . 6
5.1 General . 6
5.2 Definition . 6
5.2.1 Concept 1 (net) . 6
5.2.2 Concept 2 (marking of a net) . 6
5.2.3 Concept 3 (marked net) . 6
5.2.4 Concept 4 (precondition of a transition) . 6
5.2.5 Concept 5 (postcondition of a transition) . 6
5.2.6 Notation 1 (precondition and postcondition of a transition) . 7
5.3 Behavioral semantics. 7
5.3.1 General. 7
5.3.2 Concept 6 (net enabling rule) . 7
5.3.3 Concept 7 (net firing rule) . 7
6 Place/Transition nets . 8
6.1 General . 8
6.2 Definition — Concept 8 (place/transition net) . 8
6.3 Behavioral semantics. 8
6.3.1 General. 8
6.3.2 Concept 9 (marking of a P/T net) . 8
6.3.3 Concept 10 (P/T net enabling rule) . 9
6.3.4 Concept 11 (enabling function of enabled transitions). 9
6.3.5 Concept 12 (P/T net firing rule). 9
7 Symmetric nets . 9
7.1 Definition . 9
7.1.1 Concept 13 (color class) . 9
7.1.2 Concept 14 (color domain) . 9
7.1.3 Concept 15 (symmetric net) . 9
7.1.4 Concept 16 (basic color functions) .10
7.1.5 Concept 17 (class color functions) .10
7.2 Behavioral semantics.11
7.2.1 Concept 18 (marking of a symmetric net) .11
7.2.2 Concept 19 (symmetric net enabling rule) .11
7.2.3 Concept 20 (symmetric net firing rule) .11
8 High-level Petri nets .11
8.1 General .11
8.2 Definition — Concept 21 (high-level Petri net) .11
© ISO/IEC 2019 – All rights reserved iii

8.3 Behavioral semantics.12
8.3.1 Concept 22 (marking of a high-level Petri net) .12
8.3.2 Concept 23 (high-level Petri net enabling rule) .12
8.3.3 Concept 24 (high-level Petri net firing rule) .12
9 Petri nets with priorities.12
9.1 General .12
9.2 Definition .12
9.2.1 Concept 25 (dynamic prioritized Petri net) .12
9.2.2 Concept 26 (statically prioritized Petri net) .13
9.3 Behavioral semantics.13
9.3.1 Concept 27 (marking of a prioritized Petri net) .13
9.3.2 Concept 28 (prioritized Petri net enabling rule) .13
10 Time Petri nets .14
10.1 General .14
10.2 Definition .14
10.2.1 Concept 29 (generic time Petri net) .14
10.2.2 Concept 30 (time Petri net) .14
10.3 Behavioral semantics.14
10.3.1 General.14
10.3.2 Concept 31 (time Petri net enabling rule) .15
10.3.3 Concept 32 (time Petri net firing rule) .15
Annex A (normative) Mathematical conventions .16
Annex B (informative) Guidelines for graphical notations .20
Bibliography .29
iv © ISO/IEC 2019 – All rights reserved

Foreword
ISO (the International Organization for Standardization) and IEC (the International Electrotechnical
Commission) form the specialized system for worldwide standardization. National bodies that
are members of ISO or IEC participate in the development of International Standards through
technical committees established by the respective organization to deal with particular fields of
technical activity. ISO and IEC technical committees collaborate in fields of mutual interest. Other
international organizations, governmental and non-governmental, in liaison with ISO and IEC, also
take part in the work.
The procedures used to develop this document and those intended for its further maintenance are
described in the ISO/IEC Directives, Part 1. In particular, the different approval criteria needed for
the different types of document should be noted. This document was drafted in accordance with the
editorial rules of the ISO/IEC Directives, Part 2 (see www .iso .org/directives).
Attention is drawn to the possibility that some of the elements of this document may be the subject
of patent rights. ISO and IEC shall not be held responsible for identifying any or all such patent
rights. Details of any patent rights identified during the development of the document will be in the
Introduction and/or on the ISO list of patent declarations received (see www .iso .org/patents) or the IEC
list of patent declarations received (see http: //patents .iec .ch).
Any trade name used in this document is information given for the convenience of users and does not
constitute an endorsement.
For an explanation of the voluntary nature of standards, the meaning of ISO specific terms and
expressions related to conformity assessment, as well as information about ISO's adherence to the
World Trade Organization (WTO) principles in the Technical Barriers to Trade (TBT) see www .iso
.org/iso/foreword .html.
This document was prepared by Joint Technical Committee ISO/IEC JTC 1, Information technology,
Subcommittee SC 7, Software and systems engineering.
This second edition cancels and replaces the first edition (ISO/IEC 15909-1:2004), which has been
technically revised.
The main change compared to the previous edition is as follows:
— a complete redrafting of the concepts and definitions of Petri nets and Petri net types in a simpler,
modular and incremental way.
A list of all parts in the ISO/IEC 15909 series can be found on the ISO website.
Any feedback or questions on this document should be directed to the user’s national standards body. A
complete listing of these bodies can be found at www .iso .org/members .html.
© ISO/IEC 2019 – All rights reserved v

Introduction
The ISO/IEC 15909 series is concerned with defining a modeling language and its transfer format,
known as high-level Petri nets. This document is Part 1 of the ISO/IEC 15909 series. This document
provides the mathematical definition of high-level Petri nets, called the semantic model, its execution
semantics, the graphical form of the technique and its mapping to the semantic model. This document
also introduces some common notational conventions for the graphical form of high-level Petri nets.
Petri nets have been used to describe a wide range of systems since their invention in 1962. The
technique is mathematically defined and can thus be used to provide unambiguous specifications
and descriptions of applications. It is also an executable technique, allowing specification prototypes
to be developed to test ideas at the earliest and cheapest opportunity. Specifications written in the
technique can be subjected to analysis methods to prove properties about the specifications, before
implementation commences, thus saving on testing and maintenance time and providing a high level of
quality assurance.
A problem with Petri nets is the explosion of the number of elements in their graphical form when they
are used to describe complex systems. High-level Petri nets were developed to overcome this problem
by introducing higher-level concepts, such as the use of complex structured data as tokens, and using
algebraic expressions to annotate net elements. The use of “high-level” to describe these Petri nets
is analogous to the use of “high-level” in high-level programming languages (as opposed to assembly
languages), and is the usual term used in the Petri net community. Two of the early forms of high-level
nets that this document builds on are predicate-transition nets and coloured Petri nets, first introduced
in 1979 and developed during the 1980s. It also uses some of the notions developed for algebraic Petri
nets, first introduced in the mid-1980s. It is believed that this document captures the spirit of these
earlier developments (see Bibliography).
The technique has multiple uses. For example, it can be used directly to specify systems or to define
the semantics of other less formal languages. It can also serve to integrate techniques currently used
independently such as state-transition diagrams and data flow diagrams. The technique is particularly
suited to parallel and distributed systems development as it supports concurrency. The technique is
able to specify systems at a level that is independent of the choice of implementation (i.e. by software,
hardware (electronic and/or mechanical) or humans or a combination). This document may be cited
in contracts for the development of systems (particularly distributed systems) or used by application
developers or Petri net tool vendors or users.
This document provides an abstract mathematical syntax and a formal semantics for the technique.
Conformance to the document is possible at several levels. The level of conformance depends on the
class of high-level net chosen.
This document is Part 1 of the ISO/IEC 15909 series. It describes definitions, semantics, execution and
graphical notations for high-level Petri nets. A transfer format for the high-level Petri nets is the subject
of Part 2, while Part 3 addresses techniques for enrichments, extensions and structuring mechanisms.
Reliable software development requires powerful mathematical models and tools. The usability of Petri
nets has been proven for non-trivial industrial applications.
This document is written as a reference for systems analysts, designers, developers, maintainers and
procurers, and for Petri net tool designers and developers.
This document defines high-level Petri nets showing common concepts for Petri nets first, and then
describing several typical types of Petri nets, such as place/transition nets, symmetric nets, and Petri
nets with time. Each of the Petri net types is described with its definition, semantics, and execution.
Their graphical notations are provided in Annex B.
vi © ISO/IEC 2019 – All rights reserved

INTERNATIONAL STANDARD ISO/IEC 15909-1:2019(E)
Systems and software engineering — High-level Petri nets —
Part 1:
Concepts, definitions and graphical notation
1 Scope
This document defines a Petri net modeling language or technique, called high-level Petri nets, including
its syntax and semantics. It provides a reference definition that can be used both within and between
organizations, to ensure a common understanding of the technique and of the specifications written
using the technique. This document also facilitates the development and interoperability of Petri net
computer support tools.
This document is applicable to a wide variety of concurrent discrete event systems and in particular
distributed systems. Generic fields of application include:
— requirements analysis;
— development of specifications, designs and test suites;
— descriptions of existing systems prior to re-engineering;
— modeling business and software processes;
— providing the semantics for concurrent languages;
— simulation of systems to increase confidence;
— formal analysis of the behavior of systems;
— and development of Petri net support tools.
This document can be applied to the design of a broad range of systems and processes, including
aerospace, air traffic control, avionics, banking, biological and chemical processes, business processes,
communication protocols, computer hardware architectures, control systems, databases, defense
command and control systems, distributed computing, electronic commerce, fault-tolerant systems,
games, hospital procedures, information systems, Internet protocols and applications, legal processes,
logistics, manufacturing systems, metabolic processes, music, nuclear power systems, operating
systems, transport systems (including railway control), security systems, telecommunications and
workflows.
2 Normative references
The following documents are referred to in the text in such a way that some or all of their content
constitutes requirements of this document. For dated references, only the edition cited applies. For
undated references, the latest edition of the referenced document (including any amendments) applies.
ISO/IEC 15909-2, Systems and software engineering — High-level Petri nets — Part 2: Transfer format
3 Terms and definitions
For the purposes of this document, the terms and definitions given in ISO/IEC 15909-2 and the
following apply.
© ISO/IEC 2019 – All rights reserved 1

ISO and IEC maintain terminological databases for use in standardization at the following addresses:
— ISO Online browsing platform: available at https: //www .iso .org/obp
— IEC Electropedia: available at http: //www .electropedia .org/
3.1
arc
directed edge of a net which may connect a place (3.28) to a transition (3.37) or a transition to a place,
normally represented by an arrow
3.2
arc annotation
expression that may involve constants, variables and operators (3.21) used to annotate an arc (3.1) of a net
Note 1 to entry: The expression shall evaluate to a multiset (3.17) over the type of the arc’s associated place (3.28).
3.3
basis set
set of objects used to create a multiset (3.17)
3.4
carrier
set of a many-sorted algebra (3.14)
3.5
concurrent enabling
state, for a multiset (3.17) of transition (3.37) modes, when all the involved input
places (3.13) contain enough tokens to satisfy the sum of all of the demands imposed on them by each
input arc (3.12) annotation (3.2) evaluated for each transition mode in the multiset
3.6
concurrency
property of a system in which events may occur independently of each other, and hence are not ordered
Note 1 to entry: See also step and concurrent enabling (3.5).
3.7
declaration
set of statements which define the sets, constants, parameter (3.24) values, typed variables and
functions required for defining the annotations on a high-level Petri net (3.9)
3.8
enabling
state of a transition (3.37) in a particular mode and net marking (3.15) when the following
conditions are met: the marking of each input place (3.13) of the transition satisfies the demand imposed
on it by its arc annotation (3.2) evaluated for the particular transition mode; the demand is satisfied
when the place’s marking contains (at least) the multiset (3.17) of tokens indicated by the evaluated arc
annotation; the determination of transition modes guarantees that the Transition Condition is satisfied
Note 1 to entry: See concurrent enabling (3.5).
3.9
high-level Petri net
high-level net
HLPN
algebraic structure comprising: a set of places (3.28); a set of transitions (3.37); a set of types; a
function associating a type to each place, and a set of modes (a type) to each transition; a pre-function
imposing token demands (multisets (3.17) of tokens) on places for each transition mode; a post-function
determining output tokens (multisets of tokens) for places for each transition mode; and an initial
marking (3.10)
2 © ISO/IEC 2019 – All rights reserved

3.10
initial marking
set of initial making of places (3.11) given with the high-level net (3.9) definition
3.11
initial marking of place
special marking (3.15) of a place (3.28), defined with the net
3.12
input arc
arc directed from a place (3.28) to the transition (3.37)
3.13
input place
place (3.28) connected to the transition (3.37) by an input arc (3.12)
3.14
many-sorted algebra
mathematical structure comprising a set of sets and a set of functions taking these sets as domains and
co-domains
3.15
marking
set of the place (3.28) markings for all places of the net.
3.16
marking of a place
multiset (3.17) of tokens associated with (‘residing in’) the place (3.28)
3.17
multiset
bag
collection of items where repetition of items is allowed
3.18
multiplicity
natural number (i.e. non-negative integer) which describes the number of repetitions of an item in a
multiset (3.17)
3.19
multiset cardinality
cardinality of a multiset
sum of the multiplicities of each of the members of the multiset (3.17)
3.20
node
vertex of a net graph, i.e. either a place (3.28) or a transition (3.37)
3.21
operator
symbol representing the name of a function
3.22
output arc
arc directed from the transition (3.37) to a place (3.28)
3.23
output place
place (3.28) connected to the transition (3.37) by an output arc (3.22)
© ISO/IEC 2019 – All rights reserved 3

3.24
parameter
symbol that can take a range of values defined by a set
Note 1 to entry: It is defined as a constant in the signature (3.32).
3.25
Petri net
net
algebraic structure with two sets, one called places (3.28) and the other called transitions (3.37),
together with their associated relations and functions, and named after their inventor, Carl Adam Petri
3.26
Petri net with priorities
Petri net (3.25) having priorities which can be used for selecting the enabled transitions (3.37) according
to the given priority scheme
Note 1 to entry: The firing rule is the same as a Petri net without priorities.
3.27
Petri net with time
Petri net (3.25) having timing constraints associated with the nodes (3.20) or arcs
Note 1 to entry: These constraints affect the enabling (3.8) and firing rules.
3.28
place
node (3.20) of a net, usually represented by an ellipse
3.29
place/transition net
P/T net
Petri net (3.25) comprising a net with positive integers associated with arcs and an initial marking
(3.10) function which associates a natural number of simple tokens (‘black dots’) with places (3.28)
3.30
reachability graph
directed graph where the nodes (3.20) correspond to reachable markings (3.31) and the edges to
transition (3.37) occurrences
3.31
reachable marking
marking (3.15) of the net that can be reached from the initial marking (3.10) by the occurrence of
transitions (3.37)
3.32
signature
mathematical structure comprising a set of sorts (3.33) and a set of operators (3.21)
3.33
sort
symbol representing the name of a set
3.34
symmetric net
high-level Petri net (3.9) where types are finite and only built-in operations are allowed
3.35
term
expression comprising constants, variables and operators (3.21) built from a signature (3.32) and a set
of sorted variables
4 © ISO/IEC 2019 – All rights reserved

3.36
time Petri net
Petri net (3.25) with time where timing constraints are associated with transitions (3.37)
3.37
transition
node (3.20) of a net, usually represented by a rectangle
4 Conformance
4.1 General
There are different levels of conformance to this document. The level of conformance is defined
according to the net type.
4.2 Mandatory conformance: common concepts for Petri nets
Prior to claim conformance to any type of Petri net, defined in this document, an implementation shall
demonstrate that it has the semantics and the execution mechanisms defined in Clause 5.
4.3 Place/Transition nets
To claim P/T net Level conformance to this document an implementation shall demonstrate that it has
the semantics and the execution defined in Clause 6, by providing a mapping from the implementation
to the semantic model and the execution.
4.4 Symmetric nets
To claim Symmetric net Level conformance to this document an implementation shall demonstrate
that it has the semantics and the execution defined in Clause 7, by providing a mapping from the
implementation to the semantic model and the execution.
4.5 High-level Petri nets
4.5.1 Level 1
To claim high-level Petri net Level 1 conformance to this document an implementation shall demonstrate
that it has the semantics and the execution defined in Clause 7 (Symmetric nets), by providing a mapping
from the implementation to the semantic model and the execution.
4.5.2 Level 2
To claim high-level Petri net Level 2 conformance to this document an implementation shall have
satisfied the requirements of high-level Petri net Level 1 conformance, and in addition shall comply
with the definition and semantics defined in Clause 8.
4.6 Petri nets with priorities
To claim Petri nets with priorities conformance to this document an implementation shall demonstrate
that it has the semantics, the execution, and the prioritized Petri net model defined in Clause 9, by
providing a mapping from the implementation to the semantic model and the execution.
© ISO/IEC 2019 – All rights reserved 5

4.7 Petri nets with time — Level 1
To claim Petri nets with time Level 1 conformance to this document an implementation shall
demonstrate that it has the semantics, the execution, and the time Petri net model defined in Clause 10,
by providing a mapping from the implementation to the semantic model and the execution.
IMPORTANT — This document only defines a single type of Petri nets with time among the
many variants available. It corresponds to the semantics defined by Merlin in 1974, which is the
most commonly used. Other types of Petri nets with time can still be defined using tool-specific
information.
5 Common concepts for Petri nets
5.1 General
All common concepts for Petri nets in this Clause, and Petri net types in subsequent Clauses 6 to 10,
shall be defined using the mathematical conventions in Annex A.
5.2 Definition
5.2.1 Concept 1 (net)
A net is defined by a triple N = , where:
— P is a set of elements called places,
— T is a set of elements called transitions, disjoint from P,
— F is a flow relation FP⊆×()TT∪×()P .
If P and T are finite, then N is said to be finite.
5.2.2 Concept 2 (marking of a net)
A marking of a net N is a mapping MP: →MS , where MS is a multiset (see A.5). A place p is said to be
marked by a marking M if M(p) is not an empty multiset.
5.2.3 Concept 3 (marked net)
A marked net is a tuple N = , where is a net and M a marking of this net.
By convention, the initial marking of a marked net N is noted M .
By convention, the set of possible marked nets derived from N is noted N.
5.2.4 Concept 4 (precondition of a transition)
A place pP∈ is a precondition of the transition tT∈ iff ()pt, ∈F .
5.2.5 Concept 5 (postcondition of a transition)
A place pP∈ is a postcondition of the transition tT∈ iff ()tp, ∈F .
6 © ISO/IEC 2019 – All rights reserved

5.2.6 Notation 1 (precondition and postcondition of a transition)
Let •t and t• be respectively:
— the subset of places which constitute the precondition of a transition tT∈ (also called preset),
— the subset of places which constitute the postcondition of a transition tT∈ (also called postset).
Let us assume:
— A net consists of two different kinds of sets P and T corresponding respectively to the set of places
and the set of transitions.
— The flow relation F defines arcs connecting places to transitions, and transitions to places. There is
an arc from a place pP∈ to a transition tT∈ iff p is a precondition of t and there is an arc from a
transition tT∈ to a place pP∈ iff p is a postcondition of t.
— The marking of a place M(p) is a collection of items associated with the place p. The items associated
with places are called tokens.
— A net marking is the vector of all place markings (assuming an arbitrary order on the places).
5.3 Behavioral semantics
5.3.1 General
A Petri net has a strong behavioral semantics allowing to "execute" unambiguously the specification,
thus producing a so-called reachability graph, or marking graph, that represents all the possible
configurations the modeled system can have. This reachability graph can be infinite or finite, depending
on the characteristics of the model (boundedness). Such an execution is useful to analyze the behavior
[6]
of a system; this technique is called Model Checking .
The behavioral semantics of a Petri net relies on two notions: (i) the enabling rule, and (ii) the firing
rule. This subclause defines them in a generic way. Clauses 6 to 10 will instantiate these notions for the
types of Petri net defined by this document.
The common enabling rule in the context of interleaving semantics for all net types is defined as follows.
5.3.2 Concept 6 (net enabling rule)
Let EN: ×→TB be the enabling function of a net, which has two parameters: a net within a marked net
type NP=∈,,TF ,MN and the transition tT∈ to which it applies. M of NN∈ denotes the current
marking of N. E is defined as follows:
True whentisfirable

EN∈∈Nt,:T
()

Falseotherwise

5.3.3 Concept 7 (net firing rule)
The firing rule is defined as computed by the following steps:
1. Computation of T', the set of enabled transitions. T' is the subset of T for which
EN∈∈Nt, TT= rue .
()
i
2. Selection of an action, which can be either t in T', or some action A- (such as the elapse of time as
pre
in the case of time Petri nets).
© ISO/IEC 2019 – All rights reserved 7

3. Update of the state of net N, and, possibly some action A- (such as a reset arc emptying a place
post
from its tokens).
By default, A- and A- are the identity function. They are placeholders to host additional actions
pre post
required to capture the semantics of subsequently defined Petri net types (e.g. in time Petri nets in
Clause 10}, A- is the elapse of time).
pre
When not otherwise stated, in the subsequent Petri net types definitions, these functions are empty.
For each particular type of net, the appropriate action A- will be defined, as well as the corresponding
state update, in the appropriate section.
6 Place/Transition nets
6.1 General
Place/Transition nets are the most widely-used type of Petri nets. This clause provides their formal
definition, semantics and execution.
6.2 Definition — Concept 8 (place/transition net)
A place/transition net (P/T net) is defined by a tuple PT = , where:
— N = is a net,
— W is the arc annotation function WF: → ,
P
— M is a vector in  defining the initial number of tokens in places (initial marking).
From these definitions, the enabling and firing rules for P/T nets are defined as follows.
6.3 Behavioral semantics
6.3.1 General
A transition is enabled with respect to a net marking. A net marking comprises the set of all place
markings of the net.
Enabling a transition involves the marking of its input places. An input place of a transition is a place
which is connected to the transition by an arc leading from that place to the transition. An arc that leads
from an input place to a transition is called an input arc of the transition. If each input place’s marking
contains at least its input arc’s weight of tokens, then the transition is enabled.
Two transitions can be concurrently enabled for a particular marking, if for the associated transitions,
each input place’s marking contains at least the sum of the enabling tokens of each input arc associated
with that input place.
Enabled transitions can be fired (or occurs). When a transition is fired, tokens are removed from its
input places, and tokens are added to its output places. An output place of a transition is a place which is
connected to the transition by an arc directed from the transition to the place. An arc that leads from a
transition to a place (an output place of the transition) is called an output arc of the transition.
A place may be both an input place and an output place of the same transition.
6.3.2 Concept 9 (marking of a P/T net)
P
A marking M of a P/T net is a vector M∈ such that M(p) is the marking of place p. A marked P/T net
is a tuple PT = , where M denotes a marking of the net.
8 © ISO/IEC 2019 – All rights reserved

6.3.3 Concept 10 (P/T net enabling rule)
A transition tT∈ is enabled in marking M, denoted by , Mt[ > iff ∀∈pt• ,,Mp ≥Wp t .
() ()
From the definition above, the enabling function for P/T nets is defined as follows.
6.3.4 Concept 11 (enabling function of enabled transitions)
True iffp∀∈•tM,,()pW≥ ()pt

EN()∈∈Nt,:T

pt
Falseotherwise

6.3.5 Concept 12 (P/T net firing rule)
If a transition tT∈ is enabled in marking M, it can fire leading to a successor marking M', denoted by
Mt['>M , where: ∀∈pP ,'Mp()=Mp()−Wp(),,tW+ ()tp . This corresponds to the update of the state
of the net.
On the occurrence of a transition, the following actions occur atomically:
a) for each input place of the transition: the enabling tokens of the input arc are subtracted from the
input place’s marking, and
b) for each output place of the transition: tokens are added to the marking of the output place
according to the weight of the output arc.
7 Symmetric nets
7.1 Definition
7.1.1 Concept 13 (color class)
Let C be a non-empty finite set. A non-empty finite color class Cl over C defines a type over C. C is the
carrier set of Cl. The elements of a color class Cl may be linearly ordered, circular or unordered.
Let us remark:
— The order on the carrier set C of Cl is a total order.
— Cl being circular subsumes Cl being linearly ordered, with the additional successor function
defined below.
7.1.2 Concept 14 (color domain)
n
A color domain D is a finite cartesian product of n color classes: DC= l .
∏ i
i=1
7.1.3 Concept 15 (symmetric net)
A symmetric net (SN) is a tuple SN= NW,,Cl ,,C Φ where:
— N is a net,
— Cl=…CC, is a finite set of finite classes, each being partitioned into s static sub-classes (
{}
1, k i
CC= ),
iq=1.,si q
i
© ISO/IEC 2019 – All rights reserved 9

— C is a mapping which defines for each place and each transition its color domain,
— W is the weight function which associates with each pair ()pt, ∈×PT and each pair ()tp, ∈×TP a
general color function defined from C(t) to BagC()p ,
()
— Φ is a mapping that associates a guard with each transition.
In symmetric nets, arcs are labelled by color functions which select tokens in adjacent places depending
on the instantiation performed for the firing.
j
The simplest color functions are the projections, denoted Xi,.∈∈11.,kj .e , that select one component
i
C
i
j
of a color, the successor functions, denoted Xi++,.∈∈11.,kj .e , that select the successor of a
i
C
i
component of a color and the "global" selections Ca. ll= c that map any color to the "sum" of colors
i ∑
cC∈
i
in class C .
i
7.1.4 Concept 16 (basic color functions)
e e
1 k
Let C be a color class and DC=×…×C a color domain. The basic color functions are defined from
i 1
k
e e
1,
1 1 k
D to BagC() by for all cc=…,,cc,,……,c :
i 1
1 kk
j j
— Xc()=c (for all j such that 1≤≤je );
C i i
i
j j
— Xc()++= the successor of c in C (C is supposed to be ordered and j is such that 1≤≤je );
i i i i
C
i
— Ca. ll()cx=∑ and Ca. ll()cx=∑
i iq,
IMPORTANT — The all function is a constant function. It can thus be viewed as a constant bag
and used to define (initial) markings.
The color functions ranging over a class are obtained by linear combinations of basic color functions
(some constraints are required to ensure that the color functions select a positive number of tokens).
7.1.5 Concept 17 (class color functions)
e e
1 k
Let C be a class color and DC=×…×C be a color domain. A color function from D to BagC() is a
i 1 k i
linear combination
k k
fX=+αβ. Ca.ll + γ X ++
C ∑∑ik, iq,,iq ∑ ik,
C CC
i
i i
ke==11. qs. ke=1.
i ii
such that ∀∈dD,,∀∈cC fd c ≥0 .
()()
iC
i
Some simple constraints on α ,β and γ can be defined to ensure that fd c is positive
()()
ik, iq, ik, C
i
for all cC∈ .
i
 
For instance, the constraint: ∀∈qs11. ,.∀⊆Ke{}., βα+∑Min ,γ ≥0 achieves this goal.
()
ii iq,,ik ik,
 
10 © ISO/IEC 2019 – All rights reserved

There is an arc annotated with an expression f from a place pP∈ to a transition tT∈ iff Wp(),tf=
C C
i i
with f ≠undefined and there is an arc from a transition tT∈ to a place pP∈ iff
C
i
Wt(),pf=≠withfundefined .
CC
ii
7.2 Behavioral semantics
7.2.1 Concept 18 (marking of a symmetric net)
A marking M of a symmetric net is a vector M in BagC()()p such that M(p) is the marking of place p.
A marked symmetric net is a tuple SN= NW,,Cl,,CMΦ , where M denotes the initial marking of
0 0
the net.
7.2.2 Concept 19 (symmetric net enabling rule)
A transition tT∈ is enabled in marking M, denoted by Mt[ > , iff: ∀∈pt• ,,Mp()≥Wp(
...