Course and Tutorials

The Petri Net Course takes place from Sunday 25 to Tuesday 27.

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/or new developments presented by experts in the area. 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).

Sunday, 25 June 2023

Basic net classes

Date: Sunday, 25 June 2023
Time: 9:00–10:30 and 11:00–12:30
Room: 110-IV

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 are presented to establish structural properties of nets.

Coloured Petri nets and the CPN Tools

Date: Sunday, 25 June 2023
Time: 13:30–15:00 and 15:30–17:00
Room: 110-IV

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.

Monday, 26 June 2023

Verification and model checking of Petri Nets

Date: Monday, 26 June 2023
Time: 9:00–10:30 and 11:00–12:30
Room: 110-IV

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 course, 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.

Timed and Stochastic Petri nets

Date: Monday, 26 June 2023
Time: 14:00–15:30 and 16:00–17:30
Room: 110-IV

This module presents different ways to introduce time in Petri nets. The focus will be on two kinds of models: (1) either a time is non deterministically chosen, or (2) it is chosen based on a probability distribution. The two main models associated with non deterministic choices are time Petri nets (TPN) where time is associated with a delay for transition firings and timed Petri nets (TdPN) where time is associated with the age of tokens. We introduce the syntax and semantics of both models and we develop some standard analysis techniques. In generalized stochastic Petri nets (GSPN) the delay for transition firings is obtained by sampling a random variable. For particular kinds of distributions, we describe the construction of a continuous time Markov chain 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.

Tuesday, 27 June 2023

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

  • Luis Gomes (NOVA University Lisbon)
  • Fernando Pereira (Instituto Superior de Engenharia de Lisboa)
  • Filipe Moutinho (NOVA University Lisbon)
  • João Paulo Barros (Instituto Politécnico de Beja)
  • Anikó Costa (NOVA University Lisbon)

Date: Tuesday, 27 June 2023
Time: 9:00–10:30, 11:00–12:30, 14:00–15:30, and 16:00–17:30
Room: 110-IV

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.