SWEN90004
Modelling Complex Software Systems
Lecture Con.12 Petri Nets I: Systems and Semantics
Artem Polyvyanyy, Nic Geard
artem.polyvyanyy@unimelb.edu.au; nicholas.geard@unimelb.edu.au
Semester 1, 2021
1 / 25
Outline
Introduction to Petri nets and elementary net systems
Semantics of net systems
2 / 25
How it began
It is generally not possible to predict how much space calculations of a recursive function will consume
The data processing system that performs recursive calculations should be expandable if the available resources are insufficient for completing a calculation
Expanding a system is more efficient than starting over with a larger system
How can a system architecture that can be expanded indefinitely be described?
Every expansion of such an expandable architecture enlarges system in space
Hence, such an indefinitely expandable system must be characterized by:
No central components
No central, synchronizing clock
3 / 25
How it began
In his famous dissertation “Kommunikation mit Automaten” (Communication with Automata), Carl Adam Petri shows how to construct an indefinitely expandable asynchronous system architecture
Petri’s systems are composed of locally confined components communicating with each other via local interfaces – actions with locally confined causes and effects
Only later when Petri started to use a graphical representation of his systems the term “Petri net” was coined
So, Petri’s dissertation does not contain a single Petri net!
Petri nets is one of the most popular concepts in computer science
Legends say that Petri invented Petri nets in August 1939 at the age of 13 for the purpose of describing chemical processes
4 / 25
Components of a net structure
A Petri net is a directed graph with two types of nodes: places and transitions Places
A place p is a passive system component
Graphically represented as a circle or ellipse
A place has discrete states and can store things
Transitions
A transition t is an active system component
Graphically represented as a square or rectangle
A transition consumes, produces, or transports things
Arcs
An arc is not a system component but a logical relation between system components
Graphically represented as an arrow
An arc relates a place to a transition or a transition to
a place (bipartite graph)
5 / 25
Net structures
Sets of places, transitions, and arcs of a Petri net are customary denoted by , , and , respectively. As arcs model a relation between places and transitions, is denotedbyarelation⊆ × ∪ × .Then,
= (,,)
is a net structure. Places and transitions are the elements of , and is the flow
relation of .
Figure: A net structure (,,) with = A,B,C,D,E,F,G,H , = a,b,c,d,e , and = a,B, a,D, a,E, a,F, A,a, E,a, G,a,… .[3]
6 / 25
Markings
A marking encodes a state of a system and is an arrangement of tokens across places of a net structure.
A token can represent a thing from the real-world that can be consumed, produced, or transferred by a transition
Tokens
A token can indicate a condition that is satisfied for an occurrence of a transition
Graphically drawn as black dots inside circles and ellipses that depict places
A symbolic token can denote a token that refers to a concrete thing (e.g.,,, and)
Elementary net systems only use black dot tokens (i.e., tokens abstract from the nature of things they represent).
7 / 25
Elementary net systems
An elementary net system is a pair , , where = ,, is a net structure with finite sets of places and transitions that are disjoint (i.e., ∩ = ∅) and ∶ → N# is an initial marking.
N# is the set of all natural numbers including zero (i.e., non-negative integers) Each place $ ∈ holds $ tokens
Net system merely describes current state of control flow and availability of
resources
(A)
(H)
(B)
(C)
(D) (E)
(G) (F)
Figure: An abstract model of a cookie vending machine in the initial marking
= A,0, B,0, C,0, D,1, E,5, F,0, G,1, H,5 or
=DEEEEEGHHHHH.[3]
8 / 25
Pre-set and post-set of an element
Given a net structure , , , the pre-set ) and the post-set ) of an element ) ∈ ∪ are defined as follows:
)=*+, -∈∪ -,) ∈ and )=*+, -∈∪),-∈.
p1 p2
p5 p4
p3 (a)
p3 (b)
p5
p1
p4
p2
Figure: Examples of (a) the pre-set t and (b) the post-set t of transition t.[3]
9 / 25
The transition enablement rule
Given a net system , , where = ,, , marking enables transition 0 ∈ ifeveryplaceinthepre-setof0containsatleastonetoken(i.e.,∀$∈2 0: ($)≥1).
enabled
Figure: The only enabled transition of the cookie vending machine.
10 / 25
The step rule of elementary net systems
An enabled transition 0 can occur. An occurrence of an enabled transition 0 of a net
system , results in a step
5 ′,
where marking ′ describes the next state of the system that results from by first destroying one token in every place in the pre-set of 0 and then creating one fresh token in every place in the post-set of 0.
p1 p2
p5
p1 p2
p5 p4
p4
t
p3
Figure: An example step; adapted from [3].
p3
11 / 25
An abstract model of a cookie vending machine
We will use WoPeD to explore the behavior of the presented abstract model of a cookie vending machine
You can download WoPeD from https://woped.dhbw-karlsruhe.de/
12 / 25
An abstract model of a cookie vending machine
enabled
enabled
13 / 25
enabled
insert coin
Hot and cold transitions
So far, we have assumed that an enabled transition will either eventually become disabled or occur. This is true for transitions “a”, “b”, and “return coin”, which are internal to the system. For example, a coin in the coin slot (see below) will eventually generate a signal or will be returned. We refer to such transitions as hot transitions.
However, transitions “insert coin” and “take packet” in the real-world are triggered by a customer (an external system), and it is not guaranteed whether they will ever occur. We refer to such transitions as cold transitions and denote them with 7.
Cold transitions are rare and are often found at the interface to the environment.
cold
enabled
enabled
cold
14 / 25
Outline
Introduction to Petri nets and elementary net systems
Semantics of net systems
15 / 25
Reachable markings
Foranetsystem= , ,amarking ofisareachablemarkingofifthere exists a sequence of steps
58 5: 5< ⋯ 5>?8 5> , 9 ; @A9 @
whereB∈N# and @ = .Afinalmarkingisamarkingofinwhichnohot transitions are enabled (i.e., the system can remain in a final marking forever).
Figure: A net system.[3]
Marking Reachable Final
AC D BE BDE
ADD
16 / 25
Sequential runs (occurrence sequences)
A sequential run of a net system = , is a possibly infinite sequence of steps of that starts with the initial marking .
Figure: A net system.
CDC AC→ BC→AC→⋯
58 5: 5< ⋯ 9;
We are often interested in complete sequential runs:
A finite sequential run is complete if it leads to a final marking of
An infinite sequential run is complete if no additional step can be inserted in it
The collection of all complete sequential runs of specifies its interleaving semantics.
Sequential run
Finite Complete
CDE AC→ BC→AC→D
*C AC→ AE→BE
*CD AC→ AE→BE→AE
*CDC AC→ AE→BE→AE→⋯
17 / 25
Marking graphs (reachability graphs)
The reachable markings and steps of a net system induce the marking graph of . Its nodes are the reachable markings of
Its edges are the steps between the reachable markings of
The initial marking is highlighted with an arrow leading to it
Each final marking is highlighted with a circle with a dashed borderline
Figure: Net system . Figure: The marking graph of .[3]
Each sequential run of a net system is a directed walk in the marking graph
Each directed walk in the marking graph that starts with the initial marking is a
sequential run of the corresponding net system
NB: A finite marking graph can describe an infinite collection of sequential runs. In
general, a net system can induce a very large, or even infinite, marking graph.
18 / 25
Actions
A net system can be interpreted as a collection of distributed runs. A distributed run describes the behavior more accurately but requires more effort to understand. The main building block of a distributed run is an action, which describes a step.
t
Figure: An example step; adapted from.[3]
Figure: The action that describes the above step.[3]
19 / 25
Distributed runs (processes)
A distributed run of a net system = , is a possibly infinite acyclic net structure, also called a causal net, which describes an uninterrupted part of the behavior of . Each transition 0 of such causal net, together with 0 and 0, represents an action.
Figure: A net system.
AaB BbA
A
cD
++ CCC
Figure: Three actions that compose the example distributed run.
A distributed run is complete if and only if its places without incoming arcs represent the
initial marking and its places without outgoing arcs represent a final marking.
AaBbA
C
Figure: A complete distributed run.
The collection of all complete distributed runs of specifies its concurrency semantics.
20 / 25
cD
Sequential vs distributed runs
Both systems shown below have the same complete sequential runs, namely:
CD DC ACI→ BCE→BDE and ACI→ ADE→BDE.
System FG: Independent a and b.[3] System FH: Arbitrary order of a and b.[3] However, complete distributed runs of these two net systems are distinct.
Figure: The only complete distributed Figure: One of the two complete distributed run of 9.[3] runs of ;.[3]
21 / 25
Causality and concurrency relations
Distributed runs encode causality and concurrency relations between actions. A chain of arcs from element ) to element - in a causal net specifies that
) causally precedes -, denoted by ) ↝ -.
If two elements ) and - of a distributed run are not causal (i.e., neither ) ↝ - nor - ↝ )
holds), then they are concurrent, denoted by ) || -.
So, the causality, inverse causality, and concurrency relations partition the Cartesian
product of elements of a causal net.
123
a b A B C D I9 I; IL a II↝↜↝ II↝↜↝↝ b ↜ II ↜ II ↜ ↝ ↜ ↜ ↝ A↝↝ II↝ II↝ II↝↝ B ↜ II ↜ II II II ↜ II II C II ↝ II II II ↝ II II ↝
Figure: A distributed run.
D↜↜↜ II↜ II↜↜ II I9 ↝ ↝ II ↝ II ↝ II ↝ ↝ I; ↜ ↝ ↜ II II ↝ ↜ II ↝ IL ↜ ↜ ↜ II ↜ II ↜ ↜ II
22 / 25
Petri nets is Software Engineering
Petri nets can be used to build, simulate, and analyze abstract models of software.
Concepts presented here can be used to describe the control flow of distributed
software systems and simple data structures
High-level Petri nets extend elementary nets with aspects such as stochastic and
temporal properties of transition occurrences
Figure: A simple non-sequential program for the addition of two numbers.[2]
23 / 25
Summary
Petri nets can be interpreted according to different semantics (e.g., interleaving or concurrency)
Causality and concurrency relations between actions can be modeled explicitly in Petri nets
Hence, the occurrence of actions in sequence by chance can be distinguished from a situation when the occurrence of action is a prerequisite for the occurrence of the next action
Moreover, actions that may occur in any order but never simultaneously can be distinguished from actions that can occur truly simultaneously
A Petri net can describe a system with infinitely many reachable states
Petri nets is a natural formalism for describing distributed systems (e.g.,
distributed databased and asynchronous communication protocols)
There is a rich body of knowledge on methods for verifying formal properties of systems described as Petri nets (e.g., reachability, boundedness, safeness, liveness, etc.)
24 / 25
Further Reading
1. Carl Adam Petri Kommunikation mit Automaten. Institut für Instrumentelle
Mathematik, Bonn, IIM Report No. 2 (1962)
2. Wolfgang Reisig: Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science 4, Springer 1985, ISBN 3-540-13723-8, pp. I-IX, 1-164
3. Wolfgang Reisig: Understanding Petri Nets – Modeling Techniques, Analysis Methods, Case Studies. Springer 2013, ISBN 978-3-642-33277-7, pp. I-XXVI, 1-230
4. Wil M. P. van der Aalst, Christian Stahl: Modeling Business Processes – A Petri Net- Oriented Approach. Cooperative Information Systems series, MIT Press 2011, ISBN 978-0-262-01538-7, pp. I-XII, 1-386
5. Wolfgang Reisig: Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets. Springer 1998, ISBN 3-540-62752-9
6. Javier Esparza, Keijo Heljanko: Unfoldings – A Partial-Order Approach to Model Checking. Monographs in Theoretical Computer Science. An EATCS Series, Springer 2008, ISBN 978-3-540-77425-9, pp. I-XII, 1-156
7. Jörg Desel, Javier Esparza: Free Choice Petri Nets. Issue 40 of Cambridge Tracts in Theoretical Computer Science, ISSN 0956-9103, Cambridge University Press, 1995
25 / 25