Petri Net Course - Theory & Application

The Petri Net Course is a satellite event of the 45th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2024). This course offers a thorough introduction to Petri Nets in four half-day modules on Sunday and Monday with an option of a tutorial module (Tuesday) on applications of Petri Nets and new developments presented by experts in the area. Two alternative tutorials will be offered. Each module of the course can be taken separately. In particular, the lectures on Tuesday can be followed as independent tutorials.

Credits

All Petri Net Course modules are open for everyone interested. For the course as a whole, graduate and PhD Students are the intended audience. It is possible to earn credit points (3 ECTS awarded by Leiden University, NL) on basis of successful participation in the Course including: a preparation phase before the Course; examinations for the modules of Sunday and Monday in the form of small exercises or homework; and a written report as an outcome of a project associated with the tutorial chosen for Tuesday.

For the preparation phase, students who have registered for the full course will receive in advance material containing preliminaries on the philosophy of net theory, basic notions, small examples, typical application areas, etc. For the examination of the Sunday/Monday modules, time will be available during the course. The completion of the assignment of the Tuesday module will take place after the Petri Net Course as agreed with the lecturer(s).

to the material for preparation
(for participants only)

Module: Basic Net Classes

Lecturer:	Jörg Desel FernUniversität in Hagen joerg.desel@fernuni-hagen.de
Date:	Sunday, 23 June 2024
Time:	9.00 – 10.30 and 11.00 – 12.30
Room:	M3220 at Uni Mail, Boulevard Carl-Vogt 99, 1205 Genève Attention: This is not the venue of the main conference!

This is the introductory module to the Petri Net Course and as such provides key concepts and definitions underlying almost every Petri net model. Guided by a motivating example, principles of net theory are discussed highlighting local dynamics and concurrency. Two basic net classes are introduced and investigated: Place/Transition Systems and Elementary Net (EN) Systems. We consider the occurrence rule (token game), reachability, state graph, behavioural properties like deadlock and boundedness, behavioural equivalence and normal forms. The fundamental situations causality, conflict, concurrency, and confusion are explained in the context of EN Systems. We discuss EN system behaviour in terms of sequential and non-sequential observations. Finally, basic analysis techniques to establish structural properties of nets are presented.

to the material
(for participants only)

Module: Coloured Petri Nets and the CPN Tools

Lecturer:	Lars Michael Kristensen Western Norway University of Applied Sciences Lars.Michael.Kristensen@hvl.no
Date:	Sunday, 23 June 2024
Time:	13.30 – 15.00 and 15.30 – 17.00
Room:	M3220 at Uni Mail, Boulevard Carl-Vogt 99, 1205 Genève Attention: This is not the venue of the main conference!

This module focusses on the constructs and definition of the Coloured Petri Nets (CPNs) modelling language. CPNs belong to the class of high-level Petri nets and combines Petri Nets with the functional programming language Standard ML (SML). Petri nets provides the primitives for modelling concurrency, communication, and synchronisation while SML provides the primitives for modelling data manipulation and for creating compact and parameterised models. CPNs and the supporting computer tool CPN Tools have been widely used in practice for modelling and validating a wide range of concurrent and distributed systems. Examples demonstrating the practical use of CPN modelling and verification on industrial-sized systems will be presented. Having completed this module the participants should be able to:

explain and use the basic constructs of the CPN modelling language
explain the syntax and semantics of CPNs
structure CPN models into a hierarchically related set of modules
apply CPN Tools for construction and simulation of CPN models
perform basic state space exploration and verification of CPN models

The module includes hands-on experiments with CPN Tools.

to the material
(for participants only)

Module: Verification and model checking of Petri Nets

Lecturer:	Karsten Wolf University of Rostock karsten.wolf@uni-rostock.de
Date:	Monday, 24 June 2024
Time:	9.00 – 10.30 and 11.00 – 12.30
Room:	H8-01-F at Campus Biotech, Chemin des Mines 9, 1202 Genève

In the beginning, model checking was just a set of algorithms: given a system model and a specification (written in a temporal logic), decide whether the model satisfies the specification. The problem is challenging, mainly due to the state explosion problem. State explosion can be addressed in various ways. This has led to a wealth of technology: data structures, implementations, and approaches. In this module, model checking differentiated by the application domain. For instance, the main challenge in software model checking is to find appropriate abstractions for the data structures.

Petri net model checking has developed into its own branch of model checking. It can be characterized by:

Absence of data structures (most Petri net model checkers operate on place/transition nets),
Locality, monotonicity, and linearity of the firing rule,
Presence of massive concurrency, and
Availability of results from Petri net theory.

We cover the whole spectrum from basic algorithms to state-of-the-art technology. At every stage, we show where and how our application domain Petri nets impacts the design of a Petri net model checker. We demonstrate the results using the LoLA 2 model checking tool that is freely available.

to the material
(for participants only)

Module: Timed and Stochastic Petri Nets

Lecturer:	Serge Haddad ENS Paris-Saclay haddad@lsv.fr
Date:	Monday, 24 June 2024
Time:	13.30 – 15.00 and 15.30 – 17.00
Room:	H8-01-F at Campus Biotech, Chemin des Mines 9, 1202 Genève

This module presents different ways to introduce time in Petri nets, focusing on the various policies and ideas explored in literature. In particular, four model classes will be considered in details:

Timed Transitions Petri nets (TTPN), where time is associated to transitions as firing intervals;
Stochastic Petri Nets (SPN), where transitions are associated with an exponential distribution function;
Generalized Stochastic Petri Nets (GSPN), that extend SPN with immediate activities; and
Deterministic & Stochastic Petri Nets (DSPN), that extend GSPN with arbitrary probability distribution functions associated to transition firing times.

The module will introduce the syntax and semantics of these model classes, and develop some standard analysis techniques. For particular kinds of distributions, the module will describe the construction of a continuous time Markov chain (CTMC) or of a Markov Regenerative Processed (MRgP), on which the main performance indices can be computed.

The module will include a short description of Markov chains in order to be self-contained.

to the material
(for participants only)

Tutorial: Petri nets-driven design of controllers for cyber-physical systems

Lecturer:	Luis Gomes, Anikó Costa, João Paulo Barros NOVA University Lisbon lugo@uninova.pt
Date:	Tuesday, 25 June 2024
Time:	10.30 – 12.30, 13.30 – 15.00, and 15.30 – 17.00
Room:	H8-01-C at Campus Biotech, Chemin des Mines 9, 1202 Genève

This module focuses on the model-driven design of controllers for cyber-physical systems, where Petri nets are used as the underlying model formalism. In particular, this module heavily relies on the usage and exploitation of IOPT-nets (Input-Output Place-Transition nets), a low-level class of Petri nets mainly targeted to address discrete-event-based controllers, and associated tool-chain, publicly available at http://gres.uninova.pt/IOPT-Tools/.

IOPT nets are used to describe the controller behaviour, allowing an explicit representation of constraints on input and output signals and events. Specific semantics considering maximal step execution, single server transition firings, cycle-accurate execution, and a-priori conflict resolution (using transition priorities and test arcs) support a determinist behaviour, which is of paramount importance for majority of controllers.

The IOPT-Tools cloud-based toolchain offers a complete set of tools supporting design automation for embedded controller’s development, including tools for interactive graphical IOPT nets models editing, simulation, and test (token-player, timing diagram, remote debugging), as well as a state-space generator, state-space visualization, and a query system for properties verification.

The toolchain also supports the automatic generation of execution code to be directly deployed in the controllers’ implementation platforms, such as FPGA boards, as well as Arduino, Raspberry, and other Linux-based boards. Most notably, it is possible to obtain C code and VHDL code to be directly deployed into the referred boards without writing/changing a line in the generated code.

IOPT-Tools also support net operations, namely net addition, allowing composition of sub-models, and net splitting, which in conjunction with the use of clock domains and dedicated communication channels, support the development of distributed controllers.

The module includes examples illustrating the practical use of IOPT-nets modelling and supporting implementation of controllers. Extensive hands-on experiments with IOPT-Tools will be used.

to the material
(for participants only)

Tutorial: Adequate modeling of agent-based systems with reference nets

Lecturers:	Daniel Moldt, Laif-Oke Clasen, Marcel Hansson and Karl Ihlenfeldt Universität Hamburg moldt@informatik.uni-hamburg.de
Date:	Tuesday, 25 June 2024
Time:	10.30 – 12.30, 13.30 – 15.00, and 15.30 – 17.00
Room:	H8-01-F at Campus Biotech, Chemin des Mines 9, 1202 Genève

Complex, highly interconnected sociotechnical systems integrate People, machines, bots and traditional software system components. Modeling only with objects, only with components or only with web services does not do justice to the complex relationships between these components.In the area of multi-agent systems, agents and artifacts address the different requirements in order to capture adequately the relevant properties of system components. The overall system is often viewed as a system-of-systems, which typically requires an adaptive structure.

The PAOSE approach (Petri nets, Agents and Organization-based Software Engineering) presented in this tutorial addresses the demands of this area. We will introduce modeling concepts that take most of the above aspects into account using different variants of Petri nets. The net modeling is supplemented by further modeling techniques which have Petri net-based semantics. Those models address different levels of abstraction. Communication between net components is modeled by synchronous channels with parameters, whose semantics are based on unification mechanisms of transition bindings.

Starting from the basic idea that Petri nets can be tokens of other Petri nets (nets-within-nets concept), the modeling power is gradually increased by adding high-level features. In order to do this, we use Colored Petri nets and additional concepts and then apply adapted standard software engineering modeling techniques to create agent-based Petri net models. We will show that the nets-within-nets concept supports the adaptivity of the underlying Petri net structure by instantiating nets at simulation/execution time.

The concepts presented are integrated in the Renew tool (see http://www.renew.de) which comes with an extensive modeling toolset. We will apply these tools to small models and also demonstrate the potential of the PAOSE approach and its toolset using a relatively complex example.

to the material
(for participants only)