SUNDAY – June 23, 2019 – RWTH Aachen Informatik Center
Download Program Booklet here!
Download the Conference-USB-Stick here!
09:00-12:30 Basic net classes (Jörg Desel) – Bit Room 5053 / 1
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.
13:30-17:00 Coloured Petri Nets Modelling and CPN Tools (Lars Kristensen) – Bit Room 5053 / 1
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 24, 2019 – Room Sky Lounge 1
09:00-12:30 Coloured Petri Nets II – Verification and Applications (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.
13:30-17:15 Time(d) and Stochastic Petri nets (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.
MONDAY – June 24, 2019 – Press Conference Room
PNSE`19 program
Session: 9:00 – 10:30 (Session Chair: Manuel Wimmer)
- Hans Vangheluwe – Petri Nets in Multi-Paradigm Modelling (invited talk)
- Elena Gómez-Martínez, Juan de Lara and Esther Guerra – Towards extensible structural analysis of Petri net product lines (long talk)
Session:11:00 – 12:30 (Session Chair: Daniel Moldt)
- Torsten Liebke and Karsten Wolf – Solving E (φ U ψ) using the CEGAR approach (long talk)
- Wen Zeng and Vasileios Germanos – Modelling Hybrid Cyber Kill Chain (short talk)
- Talal Alharbi and Maciej Koutny – Domain Name System (DNS) Tunneling Detection using Structured Occurrence Nets (SONs) (short talk)
- Maxi Weichenhain and Wolfgang Fengler – A Petri Net Table Model Applied to Classic and Agile Project Management (short talk)
Session: 13:30 – 15:00 (Session Chair: Ekkart Kindler)
- Jan Mendling- Quotients for Behaviour Comparisons: Monotone Precision and Recall Measures for Process Mining (invited talk)
- Piotr Chrząstowski-Wachtel, Michał Doleżek, Paweł Greipner and Tomasz Wójcicki – Petri Meta-Compiler – a Recursive Approach to System Design and Development (short talk)
- Jan Henrik Röwekamp, Matthias Feldmann, Daniel Moldt and Michael Simon – Simulating Place/Transition Nets by a Distributed, Web Based, Stateless Service (poster presentation)
- Michael Simon, Daniel Moldt, Henri Engelhardt and Sven Willrodt – A First Prototype for the Visualization of the Reachability Graph of Reference Nets (poster presentation)
Session: 15:30 – 17:00 (Session Chair: Maciej Koutny)
- Alejandro Rodríguez, Lars Michael Kristensen and Adrian Rutle – On CTL Model Checking of the MQTT IoT Protocol using the Sweep-Line Method (long talk)
- Federica Adobbati, Luca Bernardinello and Lucia Pomello – An asynchronous game on distributed Petri nets (long talk)
- Jose J. P. Z. S. Tavares and Gabriel De A. Souza – PNRD and iPNRD Integration Assisting Adaptive Control in Block World Domain (long talk)
Closing 17:00
TUESDAY – June 25, 2019 – Press Conference Room
ATAED´19 program
Session: 9:00 – 10:30
- Wolfgang Reisig – How to analyze BIG systems? (Invited talk)
- Raymond Devillers, Evgeny Erofeev, Thomas Hujsa – Synthesis of Weighted Marked Graphs from Circular Labelled Transition Systems
Session: 11:00 – 12:30
- Jörg Desel – Can a Single Transition Stop an Entire Net?
- Adrian Puerto Aubel, Carlo Ferigato, Federica Adobbati, Stefano Gandelli – Two Operations for Stable Structures of Elementary Regions
- Nassim Laga, Marwa Elleuch, Walid Gaaloul, Oumaima Alaoui Ismaili – Emails Analysis for Business Process Discovery
Session: 13:30 – 14:30
- Ronny Tredup, Christian Rosenke – On the Hardness of Synthesizing Boolean Nets
- Alessandro Berti, Wil van der Aalst – Reviving Token-based Replay: Increasing Speed While Improving Diagnostics
Closing: 14:30
Participants are invited to join the panel on the future of process mining after the closing.
TUESDAY – June 25, 2019 – Room Sky Lounge 1
09:00-17:15 Tutorial on Verification (Karsten Wolf)
Model Checking for Petri Nets – From Algorithms to Technology
In the beginning, model checking was just a set of algorithms: given a system model and a specification (written in a temporal logic), decide whether the model satisfies the specification. The problem is challenging, mainly due to the state explosion problem. State explosion can be addressed in various ways. This has led to a wealth of technology: data structures, implementations, and approaches. In this course, model checking differentiated by the application domain. For instance, the main challenge in software model checking is to find appropriate abstractions for the data structures.
Petri net model checking has developed into its own branch of model checking. It can be characterized by:
- Absence of data structures (most Petri net model checkers operate on place/transition nets),
- Locality, monotonicity, and linearity of the firing rule,
- Presence of massive concurrency, and
- Availability of results from Petri net theory.
Since 2011, progress in Petri net model checking has been propelled through the yearly Model Checking Contest.
The tutorial spans the whole spectrum from basic algorithms to state-of-the-art technology. At every stage, we show where and how our application domain Petri nets impacts the design of a Petri net model checker. We demonstrate the results using the LoLA 2 model checking tool that is freely available.
TUESDAY – June 25, 2019 – Room Sky Lounge 4
09:00-17:15 Tutorial (Ekkart Kindler)
Model – based Software Engineering for/with Petri Nets
Model-based Software Engineering (MBSE) is a catch-all term for software development technologies in which models are more than just „nice sketches“ or „drawings“. In MBSE, models are mostly used for generating some parts of the code automatically from models or for executing models directly. The OMG‘s Model Driven Architecture (MDA) is probably one of the most prominent approaches in this direction and Eclipse EMF is a very popular technology supporting MBSE. But, MBSE also covers approaches that are more focused on analyzing or verifying software models.
Petri nets have been used for modelling for a long time now and they are successfully used in different areas of software and systems development. Though Petri nets are used in all stages of software development, many approaches focus on the early phases of the development process and for building prototypes; the actual software is often still programmed manually. This course presents the idea, the main concepts, and some technologies of MBSE — with the focus on automatic code generation. On the one hand, these technologies can be used for developing Petri net tools in a more efficient way. On the other hand, they can be used to generate parts of the software automatically from Petri net models. More importantly, we will see how Petri nets and the code generated from them can be integrated with other software.
The course will be based on the experiences with Eclipse EMF and developing the ePNK based on EMF, and discuss the lessons learned with developing the ECNO Tool, which allows to generate software completely automatically from models which consists of the Event Coordination Notation and ECNO nets (which are a special version of Petri nets for modeling the life-cycle of is components).
WEDNESDAY – June 26, 2019 – Press Conference Room
Petri Nets
09:00-09:15 Opening Session (General Chair and PC chairs)
Welcome by the General Chair, introduction of program by the PC Chairs.
Opening-Petri-Net-Wednesday-PDF
09:15–10:15 Carl Adam Petri Lecture (CAP) – (Shared ACSD and Petri Nets, Session Chair: Stefan Haar)
Luca Cardelli – Programmable Molecular Networks
11:00–12:30 Synthesis (Session Chair: Thomas Chatain)
- Raymond Devillers – Articulation of Transition Systems and its Application to Petri Net Synthesis
- Ronny Tredup – Hardness Results for the Synthesis of b-bounded Petri Nets
- Ronny Tredup – Fixed Parameter Tractability and Polynomial Time Results for the Synthesis of b-bounded Petri Nets
13:30–15:00 Semantics (Session Chair: Karsten Wolf)
- David Frutos Escrig, Maciej Koutny and Lukasz Mikulski – Reversing Steps in Petri Nets
- Ryszard Janicki – On Interval Semantics of Inhibitor and Activator Nets
- Lukasz Mikulski and Ivan Lanese. – Reversing Unbounded Petri Nets
15:30–17:00 Models with extensions (Session Chair: Lukasz Mikulski)
- Alain Finkel, Serge Haddad and Igor Khmelnitsky – Coverability and Termination in Recursive Petri Nets
- Marco Montali and Andrey Rivkin – From DB-nets to Coloured Petri Nets with Priorities
- Didier Lime, Olivier H. Roux and Charlotte Seidner – Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets
18:30-20:00 (Optional: Annual IEEE Task Force on Process Mining Meeting)
19:30 Sightseeing tour
THURSDAY – June 27, 2019 – Room – Club Lounge 1
09:00–10:00 Session Chair: (Session Chair: Jörg Keller) – Invited talk ACSD (Shared ACSD and Petri nets)
Philippas Tsigas – Lock-free Data Sharing in Concurrent Software Systems
10:00–10:30 Stochastic Models (Session Chair: Anna Kalenkova)
Giulio Masetti, Leonardo Robol, Silvano Chiaradonna and Felicita Di Giandomenico
Stochastic modeling and evaluation of large interdependent composed models through Kronecker algebra and exponential sums
11:00–12:30 Concurrent Processes (Session Chair: Robert Lorenz)
- Mathilde Boltenhagen, Thomas Chatain and Josep Carmona – Generalized Alignment-Based Trace Clustering of Process Behavior
- Lisa Luise Mannel and Wil M. P. van der Aalst – Finding Complex Process-Structures by Exploiting the Token-Game
- Felix Freiberger and Holger Hermanns – Concurrent Programming from pseuCo to Petri
13:30–15:00 Algorithmic Aspects (Session Chair: Gianfranco Ciardo)
- Shruti Biswal and Andrew S Miner – Improving Saturation Efficiency with Implicit Relations
- Vince Molnár and István Majzik – Saturation Enhanced with Conditional Locality: Application to Petri Nets
- Torsten Liebke and Karsten Wolf – Taking Some Burden off an Explicit CTL Model Checker
15:30–16:50 Tools (20 minutes per talk) (Session Chair: Ekkart Kindler)
- Jan Henrik Röwekamp and Daniel Moldt – RenewKube: Reference Net Simulation Scaling with Renew and Kubernetes
- Matteo Camilli, Carlo Bellettini and Lorenzo Capra – PNemu: an Extensible Modeling Library for Adaptable Distributed Systems
- Jan Martijn Van Der Werf and Lucas Steehouwer – CoRA: an Online Intelligent Tutoring System to Practice Coverability Graph Construction
- Michael Simon, Daniel Moldt, Dennis Schmitz and Michael Haustermann – Tools for Curry-Coloured Petri Nets
16:50–17:30 Tools Demonstrations (Session Chair: Bas van Zelst)
| Presenter(s)/Developer(s) | Tool | Website/Reference |
| Frank Mueller | REALIST | http://www.ima.uni-stuttgart.de/realist |
| Felix Freiberger, Holger Hermanns | pseuCo.com | https://pseuco.com/ |
| Jan Henrik Roewekamp | RenewKube | https://paose.informatik.uni-hamburg.de/paose/wiki/RenewKube |
| Michael Simon | CCPN | https://git.informatik.uni-hamburg.de/tgipublic/ccpn/ccpn/wikis/pn19 |
| Alessandro Berti | PM4Py | http://pm4py.pads.rwth-aachen.de |
| Ekkart Kindler | ePNK | http://www2.compute.dtu.dk/~ekki/projects/ePNK/index.shtml |
| Jaime Arias | CosyVerif | http://www.cosyverif.org/documentation/ |
| Matteo Camilli | PNemu | https://github.com/SELab-unimi/pnemu |
| Jan Martijn van der Werf | Cora | NA |
FRIDAY – June 28, 2019 – Room – Club Lounge 1
09:00–10:00 Invited talk Petri nets (Shared ACSD and Petri nets) (Session Chair: Susanna Donatelli)
Dirk Fahland – Describing, Discovering, and Understanding Multi-Dimensional Processes
10:00–10:30 Open Nets: (Session Chair: Ryszard Janicki)
Walter Vogler and Vitali Schneider – Modal Open Nets
11:00–12:00 Parametrics and Combinatorics: (Session Chair: Serge Haddad
- Chana Weil-Kennedy, Mikhail Raskin and Javier Esparza – Parameterized Analysis of Immediate Observation Petri Nets
- Olivier Bodini, Matthieu Dien, Antoine Genitrini and Frederic Peschanski – The Combinatorics of Barrier Synchronization
12:00–12:30 Session: (Session Chair: Maciej Koutny)
Closing session and presentation of Petri nets 2020 in Paris
FRIDAY – June 28, 2019 – Room – Club Lounge 1
Retrospective and Perspective of Petri Net Research
On the occasion of the 40th birthday of the Petri net community, a special session will take place just after the closing of the Petri Net Conference. Outstanding speakers will reflect on the history of Petri net research and its future. This event is open to everybody and not only to participants of the Petri Net Conference.
13:30-14:50 Session 1: (Chair: Jörg Desel)
- 13:30 Wolfgang Reisig: How it all began
- 14:10 Maciej Koutny: The Petri net community today (including statistics)
15:10-16:30 Session 2: (Chair: Alex Yakovlev)
- 15:10 Gianfranco Balbo: 35 years of (generalized) stochastic Petri nets for performance analysis
- 15:30 Javier Esparza: 25 years of net unfoldings and true-concurrency analysis tools
- 15:50 Wil van der Aalst: 20 years of workflow Petri nets, initiating the biggest success story of Petri nets
- 16:10 Fabrice Kordon: 10 years of model checking contests with Petri nets
17:00-18:00 Session 3: (Chair: Jetty Kleijn)
17:00 P.S. Thiagarajan: Some thoughts on Carl Adam Petri, Petri nets, concurrency theory and biology
18.00 end
Download Program Booklet here!
Download the Conference-USB-Stick here!
