Sunday, 19 Jun | Monday, 20 Jun | Tuesday, 21 Jun
The Petri Net Course takes place from Sunday 19 to Tuesday 21.
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.
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).
Date: Sunday, 19 June 2022
Time: 9:00–12:30
Room: M125
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.
Date: Sunday, 19 June 2022
Time: 13:30–17:00
Room: M125
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:
The module includes hands-on experiments with CPN Tools.
Date: Monday, 20 June 2022
Time: 9:00–12:30
Room: M125
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:
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.
Date: Monday, 20 June 2022
Time: 14:00–17:30
Room: M125
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.