Alster

Petri Net Course – Schedule

Note: Detailed information about all events is also collected in the programme booklet.

Download
Here you can download a pdf version of the Petri Net Course Schedule.
Sunday, June 24, 2012
Module 1: Basic net classes
Lecturers: Jörg Desel and Jetty Kleijn
Room: D-125 Informatics Campus
Timeslots: 9:30 – 11:00 and 11:30 – 13:00
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.
Module 2: Coloured Petri Nets 1 (Modelling)
Lecturers: Lars Kristensen
Room: D-125 Informatics Campus
Timeslots: 14:30 – 16:00 and 16:30 – 18:00
This module focuses on the constructs and definition of the Coloured Petri Nets (CPN) 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 software systems.
Having completed this module the participants will be able to:
  • explain and use the basic constructs of the CPN modelling language
  • explain the syntax and semantics of CPNs
  • apply CPN Tools for construction and simulation of medium-sized CPN models
The module includes hands-on experiments with CPN Tools.
Monday, June 25, 2012
Module 3: Coloured Petri Nets 2 (Analysis)
Lecturers: Lars Kristensen
Room: D-125 Informatics Campus
Timeslots: 8:45 – 10:15 and 10:45 – 12:15
Explicit state space exploration is one of the main approaches to computer-aided verification of concurrent systems, and it is one of the main analysis methods for Coloured Petri Nets (CPNs). This module provides an introduction to state space methods in the context of CPNs, and explains how standard behavioural properties of CPNs can be verified fully automatically using state spaces and the support for state space analysis provided by CPN Tools.
Having completed this module the participants will be able to:
  • define standard behavioural properties of CPNs
  • explain the basic concepts of state spaces and how they are computed
  • explain how basic behavioural properties can be verified from state spaces
  • apply state spaces for verification of medium-sized CPN models
The module includes hands-on experience with CPN Tools and examples of industrial applications of state space methods.
Module 4: Timed and Stochastic Petri Nets
Lecturers: Susanna Donatelli and Serge Haddad
Room: D-125 Informatics Campus
Timeslots: 13:45 – 15:15 and 15:45 – 17:15
This module presents different ways to introduce time in Petri nets. The focus will be on two models, where time is associated with the firing delay of transitions. In time Petri nets (TPN), the delay is non-deterministically chosen within an interval. We describe the class graph construction, which is the main analysis tool of TPNs. In generalized stochastic Petri nets (GSPN) the delay 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.
Tuesday, June 26, 2012
Full Day: Choose one of the following two Tutorial Modules.
Tutorial Module 1: Fluid & Hybrid Nets
Lecturers: Manuel Silva and Cristian Mahulea
Room: C-104 Informatics Campus
Timeslots: 8:45 – 10:15, 10:45 – 12:15, 13:45 – 15:15 and 15:45 – 17:15
Details: Fluid and Hybrid Nets
Fluidization: a relaxation approach to study heavily loaded discrete event systems. Autonomous (untimed) and timed fluid models. Relations among discrete and fluid "views" of a DEDS. Limitation of the fluidization. Improvement of fluid approximations: removing spurious solutions and stochastic fluid models. Structural analysis of fluid PN models. Observability and observers. Controllability and controllers. Application examples using SimHPN toolbox.
Participants are encouraged to bring their own laptop with MATLAB installed on it if they want to use the relevant tool and get a hands-on experience.
Tutorial Module 2: Net Unfoldings
Lecturers: Thomas Chatain, Stefan Haar, Victor Khomenko, G. Michele Pinna
Room: C-215 Informatics Campus
Timeslots: 8:45 – 10:15, 10:45 – 12:15, 13:45 – 15:15 and 15:45 – 17:15
Details:Net Unfoldings Petri net unfoldings is a prominent formalism for the description and analysis of concurrent systems. This course will provide a general introduction into unfoldings, unfolding based formal verification and applications of unfoldings. These will be combined with demonstration of some practical unfolding-based tools. Moreover, a number of recent ideas will be considered in more detail, including the reveals relation, symbolic prefixes, and merged processes and related models.

<< back to course overview


Page last modified: 2012/06/24