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
