Petri Nets 2016 // ACSD 2016

International Workshop on Petri Nets and Software Engineering

For the successful realisation of complex systems of interacting and reactive software and hardware components the use of a precise language at different stages of the development process is of crucial importance. Petri nets are becoming increasingly popular in this area, as they provide a uniform language supporting the tasks of modelling, validation, and verification. Their popularity is due to the fact that Petri nets capture fundamental aspects of causality, concurrency and choice in a natural and mathematically precise way without compromising readability.

The use of Petri nets (P/T-nets, coloured Petri nets and extensions) in the formal process of software engineering, covering modelling, validation, and verification, will be presented as well as their application and tools supporting the disciplines mentioned above.

Workshop website

7th International Workshop on Biological Processes & Petri Nets (BioPPN 2016)

The goal of this workshop is to provide a platform for researchers aiming at fundamental research and real life applications of Petri nets and other concurrency models in Systems and Synthetic Biology.

Workshop website

Algorithms & Theories for the Analysis of Event Data (ATAED) 2016

The workshop aims to attract papers related to Process Mining, Region Theory and other synthesis techniques. These techniques have in common that "lower level" behavioral descriptions (event logs, partial orders, transition systems, etc.) are used to create "higher level" process models (e.g., various classes of Petri nets, BPMN, or UML activity diagrams).

Workshop website

Petri Net Course

The Petri Net Course takes place on Sunday, Monday, Tuesday June 19-21. Organisers are Jörg Desel (FernU. Hagen) and Jetty Kleijn (Leiden U.).

This course offers a thorough introduction to Petri Nets in four half-day modules on Sunday and Monday with on Tuesday a choice from two full-day tutorial module 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.

Sunday, June 19

Lecture: Basic Net Classes
Lecturer: Jetty Kleijn

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.

Lecture: Coloured Petri Nets 1 - Modelling and CPN Tools
Lecturer: Lars Kristensen

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. Having completed this module the participants should be able to:

explain and use the basic constructs of the CPN modelling language
explain the syntax and semantics of CPNs
structure CPN models into a hierarchically related set of modules
apply CPN Tools for construction and simulation of CPN models

The module includes hands-on experiments with CPN Tools.

Monday, June 20

Lecture: Coloured Petri Nets 2 - Verification and Applications
Lecturer: Lars Kristensen

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 exploration provided by CPN Tools. The module also introduces the basics of temporal logic and associated model checking algorithms for verifying more general behavioral properties of concurrent 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:

define standard behavioural properties of CPNs and express behavioral properties in temporal logic
explain the basic concepts of state spaces and how they are computed
explain how behavioural properties can be automatically checked from state spaces
apply state spaces and model checking techniques for verification of CPN models

The module includes hands-on experiments with CPN Tools.

Lecture: Time(d) and Stochastic Petri Nets
Lecturer: Serge Haddad

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.

Tuesday, June 21

Tutorial: Modelling, Synthesis and Verification of Hardware
Lecturers: Alex Yakovlev, Victor Khomenko, Andrej Mokhov, Danil Sokolov

In this tutorial we will present an up-to-date vision of and approach to applying Petri nets and related concurrency models to modelling, verification and synthesis of electronic circuits. Petri nets are seen here as a unifying modelling language for reasoning about the behaviour of digital circuits and systems, where various application-specific and engineering-specific modelling notations can be used as front-end notations. In the first half of the tutorial we will introduce theoretical aspects of our methodology, while the second half will be devoted to the familiarisation with the toolkit Workcraft, which supports (and is constantly in the process of expansion!) a range of front-end notations for digital hardware, captured at different levels of abstraction and granularity. The examples of the front end notation we will be presenting include both structurally oriented models, such as data-flow structures and logic circuit net-lists, as well a behavioural formalisms, such as state-graphs and conditional partial order graphs.

While the spectrum of hardware that can be modelled and designed includes both synchronous (aka globally clocked) and asynchronous (aka self-timed) circuits, our main focus is on the support for designing asynchronous logic. Why? The reason for that is that self-timed circuits are inherently concurrent and the role played by Petri nets for them is as fundamental as the role played by finite-state machines in traditional synchronous design. Thus, the hardware whose behavioural semantics is conveniently underpinned by Petri nets includes digital processors, pipelines, arbiters, interfaces and controllers, and most notably digital control for analog electronics, such as power converters.

Tutorial: Parametric Verification
Lecturers: Étienne André, Didier Lime, Wojciech Penczek, Laure Petrucci

Modelling languages such as Petri Nets or Timed Automata allow for designing critical systems and model-checking their expected properties. However, all characteristics of the system under construction may not be known in advance. The nature of such unknown parts is manyfold, e.g.: the designer may have the choice of different components with similar behaviour and different timing constraints; there can be an a priori unknown number of identical processes present in the system ; some actions can be controlled to be enabled or disabled, have different probabilities of occurring, etc. These situations can be captured by introducing parameters in particular on timings, actions, and probabilities.

In this tutorial, we focus on such parameterised models and their associated analysis techniques. These allow for tuning the actual values of parameters in order to satisfy expected properties. It also provides the designer with a set of adequate choices w.r.t. what the system should achieve.
The tutorial will present the underlying theory, the verification approaches, typical applications, and will put these into practice through hands-on sessions using Imitator, Spatula and Romeo tools.

Credits

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).

Model Checking Contest

The Model Checking Contest (MCC) is a yearly event that assesses existing verification tools for concurrent systems on a set of models (i.e., benchmarks) proposed by the scientific community. All tools are compared on the same benchmarks and using the same computing platform, so that a fair comparison can be made, contrary to most scientific publications, in which different benchmarks are executed on different platforms.

Model Checking Contest website


Full version Home page Important dates Satellite events Committees Program Registration In Toruń Venue Events Contact	International Workshop on Petri Nets and Software Engineering For the successful realisation of complex systems of interacting and reactive software and hardware components the use of a precise language at different stages of the development process is of crucial importance. Petri nets are becoming increasingly popular in this area, as they provide a uniform language supporting the tasks of modelling, validation, and verification. Their popularity is due to the fact that Petri nets capture fundamental aspects of causality, concurrency and choice in a natural and mathematically precise way without compromising readability. The use of Petri nets (P/T-nets, coloured Petri nets and extensions) in the formal process of software engineering, covering modelling, validation, and verification, will be presented as well as their application and tools supporting the disciplines mentioned above. Workshop website 7th International Workshop on Biological Processes & Petri Nets (BioPPN 2016) The goal of this workshop is to provide a platform for researchers aiming at fundamental research and real life applications of Petri nets and other concurrency models in Systems and Synthetic Biology. Workshop website Algorithms & Theories for the Analysis of Event Data (ATAED) 2016 The workshop aims to attract papers related to Process Mining, Region Theory and other synthesis techniques. These techniques have in common that "lower level" behavioral descriptions (event logs, partial orders, transition systems, etc.) are used to create "higher level" process models (e.g., various classes of Petri nets, BPMN, or UML activity diagrams). Workshop website Petri Net Course The Petri Net Course takes place on Sunday, Monday, Tuesday June 19-21. Organisers are Jörg Desel (FernU. Hagen) and Jetty Kleijn (Leiden U.). This course offers a thorough introduction to Petri Nets in four half-day modules on Sunday and Monday with on Tuesday a choice from two full-day tutorial module 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. Sunday, June 19 Lecture: Basic Net Classes Lecturer: Jetty Kleijn 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. Lecture: Coloured Petri Nets 1 - Modelling and CPN Tools Lecturer: Lars Kristensen 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. Having completed this module the participants should be able to: explain and use the basic constructs of the CPN modelling language explain the syntax and semantics of CPNs structure CPN models into a hierarchically related set of modules apply CPN Tools for construction and simulation of CPN models The module includes hands-on experiments with CPN Tools. Monday, June 20 Lecture: Coloured Petri Nets 2 - Verification and Applications Lecturer: Lars Kristensen 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 exploration provided by CPN Tools. The module also introduces the basics of temporal logic and associated model checking algorithms for verifying more general behavioral properties of concurrent 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: define standard behavioural properties of CPNs and express behavioral properties in temporal logic explain the basic concepts of state spaces and how they are computed explain how behavioural properties can be automatically checked from state spaces apply state spaces and model checking techniques for verification of CPN models The module includes hands-on experiments with CPN Tools. Lecture: Time(d) and Stochastic Petri Nets Lecturer: Serge Haddad 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. Tuesday, June 21 Tutorial: Modelling, Synthesis and Verification of Hardware Lecturers: Alex Yakovlev, Victor Khomenko, Andrej Mokhov, Danil Sokolov In this tutorial we will present an up-to-date vision of and approach to applying Petri nets and related concurrency models to modelling, verification and synthesis of electronic circuits. Petri nets are seen here as a unifying modelling language for reasoning about the behaviour of digital circuits and systems, where various application-specific and engineering-specific modelling notations can be used as front-end notations. In the first half of the tutorial we will introduce theoretical aspects of our methodology, while the second half will be devoted to the familiarisation with the toolkit Workcraft, which supports (and is constantly in the process of expansion!) a range of front-end notations for digital hardware, captured at different levels of abstraction and granularity. The examples of the front end notation we will be presenting include both structurally oriented models, such as data-flow structures and logic circuit net-lists, as well a behavioural formalisms, such as state-graphs and conditional partial order graphs. While the spectrum of hardware that can be modelled and designed includes both synchronous (aka globally clocked) and asynchronous (aka self-timed) circuits, our main focus is on the support for designing asynchronous logic. Why? The reason for that is that self-timed circuits are inherently concurrent and the role played by Petri nets for them is as fundamental as the role played by finite-state machines in traditional synchronous design. Thus, the hardware whose behavioural semantics is conveniently underpinned by Petri nets includes digital processors, pipelines, arbiters, interfaces and controllers, and most notably digital control for analog electronics, such as power converters. Tutorial: Parametric Verification Lecturers: Étienne André, Didier Lime, Wojciech Penczek, Laure Petrucci Modelling languages such as Petri Nets or Timed Automata allow for designing critical systems and model-checking their expected properties. However, all characteristics of the system under construction may not be known in advance. The nature of such unknown parts is manyfold, e.g.: the designer may have the choice of different components with similar behaviour and different timing constraints; there can be an a priori unknown number of identical processes present in the system ; some actions can be controlled to be enabled or disabled, have different probabilities of occurring, etc. These situations can be captured by introducing parameters in particular on timings, actions, and probabilities. In this tutorial, we focus on such parameterised models and their associated analysis techniques. These allow for tuning the actual values of parameters in order to satisfy expected properties. It also provides the designer with a set of adequate choices w.r.t. what the system should achieve. The tutorial will present the underlying theory, the verification approaches, typical applications, and will put these into practice through hands-on sessions using Imitator, Spatula and Romeo tools. Credits 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). Model Checking Contest The Model Checking Contest (MCC) is a yearly event that assesses existing verification tools for concurrent systems on a set of models (i.e., benchmarks) proposed by the scientific community. All tools are compared on the same benchmarks and using the same computing platform, so that a fair comparison can be made, contrary to most scientific publications, in which different benchmarks are executed on different platforms. Model Checking Contest website