Petri Net Course & Tutorials
The Petri Net Course takes place from Sunday to Tuesday before the conferences.
It offers a thorough introduction to Petri Nets in four half-day modules on Sunday and Monday:
- Basic Net Classes
- Coloured Petri Nets 1
- Coloured Petri Nets 2
- Timed and Stochastic Petri Nets
On Tuesday there is a choice between two full-day tutorial modules on applications of Petri Nets and/or new developments presented by experts in the area. This year the subjects are:
Each module of the course can be taken separately. In particular, the lectures on Tuesday can be followed as independent Tutorials.
Credits
All 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 theory modules in the form of small exercises or homework, and
- a written report as an outcome of a project associated with the tutorial chosen for the third day.
For the preparation phase, students who have registered for the full Course, will receive one to two weeks 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 Course as agreed with the lecturer(s).
Contact
For further information please contact the
organizers
- Jetty Kleijn (
) or
- Jörg Desel (
).
Preliminary Schedule
- Sunday, June 24, 2012
-
Morning: Basic net classes - Jörg
Desel/Jetty Kleijn
Content: Behaviour of Elementary Net
systems and relation to other models of concurrency, place /
transition nets and extensions, elementary analysis methods.
-
Afternoon: Coloured Petri Nets 1 (Modelling) -
Lars Kristensen
Content: 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
-
Morning: Coloured Petri Nets 2 (Analysis) - Lars
Kristensen
Content: 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.
-
Afternoon: Timed and Stochastic Petri Nets -
Susanna Donatelli, Serge Haddad
Content: Timed Petri Nets,
Stochastic Petri Nets
- Tuesday, June 26, 2012
-
Full Day: Choose one of the following two
Tutorial Modules.
-
Tutorial Module 1: Fluid and
Hybrid Nets - Manuel Silva, Cristian Mahulea
Details:
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: Unfoldings -
Thomas Chatain, Stefan Haar, Victor Khomenko, G. Michele Pinna
Details:
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.
