Home
• Main Events
  • Petri Nets 2014
  • ACSD 2014
• Co-located events
  • Workshops
  • Tutorials
  • Petri Net Course
  • Tools Exhibition
  • M.C. Contest
• Programme
  • Overview
  • Session Schedule
  • Keynote Speakers
  • Social Events
  • Accepted Papers
  • Proceedings
• Travel Information
  • How to reach Tunis
  • Accommodation
  • Locations
  • Sightseeing
• Registration
• Committees
• Sponsors Petri Nets
• Sponsors ACSD
• Contact

Petri Net Course

Petri Net Course: Theory & Applications (starts on 22th June)
Organisers: Jörg Desel and Jetty Kleijn

This course offers a thorough introduction to Petri Nets in four half-day modules on Sunday and Monday, June 22 and June 23 2014 and a full-day tutorial module on Tuesday, June 24.

On Tuesday there is a choice from two alternative tutorial modules with one devoted to symmetric nets and the other to Petri nets for multiscale systems biology.

For successful participation in the entire course, including preparation and examination, three credit points (ECTS) will be awarded by Leiden University (The Netherlands).

Each module of the course can also be taken separately, without any credits.

Petri Net Course Schedule

Module 1: Basic net classes
Lecturers: Joerg Desel and Jetty Kleijn
Room: Tunis Science City
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: Tunis Science City
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.


Module 3: Coloured Petri Nets 2 (Analysis)
Lecturers: Lars Kristensen
Room: Tunis Science City
Timeslots: 9:30 – 11:00 and 11:30 – 13:00

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
Lecturer: Serge Haddad
Room: Tunis Science City
Timeslots: 14:30 – 16:00 and 16:30 – 18:00

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.