Skip to main content

About this book

The 14th volume of ToPNoC contains revised and extended versions of a selection of the best workshop and tutorial papers presented at the 39th International Conference on Application and Theory of Petri Nets and Concurrency, Petri Nets 2018, and the 18th International Conference on Application of Concurrency to System Design, ACSD 2018.The 10 papers cover a diverse range of topics including model checking and system verification, refinement, and synthesis; foundational work on specific classes of Petri nets; and innovative applications of Petri nets and other models of concurrency. Application areas covered in this volume are: process mining, verification, formal semantics, communication protocols, business processes, distributed systems, and net synthesis. Thus, this volume gives a good overview of ongoing research on concurrent systems and Petri nets.

Table of Contents


A Tour in Process Mining: From Practice to Algorithmic Challenges

Process mining seeks the confrontation between modeled behavior and observed behavior. In recent years, process mining techniques managed to bridge the gap between traditional model-based process analysis (e.g., simulation and other business process management techniques) and data-centric analysis techniques such as machine learning and data mining. Process mining is used by many data-driven organizations as a means to improve performance or to ensure compliance. Traditionally, the focus was on the discovery of process models from event logs describing real process executions. However, process mining is not limited to process discovery and also includes conformance checking. Process models (discovered or hand-made) may deviate from reality. Therefore, we need powerful means to analyze discrepancies between models and logs. These are provided by conformance checking techniques that first align modeled and observed behavior, and then compare both. The resulting alignments are also used to enrich process models with performance related information extracted from the event log. This tutorial paper focuses on the control-flow perspective and describes a range of process discovery and conformance checking techniques. The goal of the paper is to show the algorithmic challenges in process mining. We will show that process mining provides a wealth of opportunities for people doing research on Petri nets and related models of concurrency.
Wil van der Aalst, Josep Carmona, Thomas Chatain, Boudewijn van Dongen

How Petri Net Theory Serves Petri Net Model Checking: A Survey

Structure theory is a unique treasure of the Petri net community. It was originally studied as a set of stand-alone techniques for exploring Petri net properties such as liveness, boundedness, reachability, and deadlock freedom. Today, methods based on the exploration of the reachability graph (state space methods) dominate Petri net verification. Thanks to the concept of model checking, these methods can deal with a much larger range of verification problems, and thanks to state space reduction methods (symmetries, partial order reduction, and other abstraction techniques), they became tractable for many practical applications. However, in the course of pushing model checking technology to its limits, several elements of Petri net structure theory celebrate a resurrection, being viewed from a different angle. This time, they are used for acceleration of the state space methods. In this article, we give an overview on the use of structural methods in Petri net model checking. We further report on our experience with combining state space and structural methods.
Karsten Wolf

Parametric Verification: An Introduction

This paper constitutes a short introduction to parametric verification of concurrent systems. It originates from two 1-day tutorial sessions held at the Petri nets conferences in Toruń (2016) and Zaragoza (2017). A video of the presentation is available at https://​www.​youtube.​com/​playlist?​list=​PL9SOLKoGjbeqNcd​QVqFpUz7HYqD1fbF​Ig, consisting of 14 short sequences. The paper presents not only the basic formal concepts tackled in the video version, but also an extensive literature to provide the reader with further references covering the area.
We first introduce motivation behind parametric verification in general, and then focus on different models and approaches, for verifying several kinds of systems. They include Parametric Timed Automata, for modelling real-time systems, where the timing constraints are not necessarily known a priori. Similarly, Parametric Interval Markov Chains allow for modelling systems where probabilities of events occurrences are intervals with parametric bounds. Parametric Petri Nets allow for compact representation of systems, and cope with different types of parameters. Finally, Action Synthesis aims at enabling or disabling actions in a concurrent system to guarantee some of its properties. Some tools implementing these approaches were used during hands-on sessions at the tutorial. The corresponding practicals are freely available on the Web.
Étienne André, Michał Knapik, Didier Lime, Wojciech Penczek, Laure Petrucci

Integrated Simulation of Domain-Specific Modeling Languages with Petri Net-Based Transformational Semantics

The development of domain specific models requires appropriate tool support for modeling and execution. Meta-modeling facilitates solutions for the generation of modeling tools from abstract language specifications. The Rmt approach (Renew Meta-Modeling and Transformation) applies transformational semantics using Petri net formalisms as target languages in order to produce quick results for the development of modeling techniques. The problem with transformational approaches is that the inspection of the system during execution is not possible in the original representation.
We present a concept for providing simulation feedback for domain specific modeling languages (DSML) that are developed with the Rmt approach on the basis of meta-models and transformational semantics using Petri nets. Details of the application of this new approach are illustrated by some well-known constructs of the Business Process Model and Notation (BPMN).
David Mosteller, Michael Haustermann, Daniel Moldt, Dennis Schmitz

Formal Modelling and Incremental Verification of the MQTT IoT Protocol

Machine to Machine (M2M) communication and Internet of Things (IoT) are becoming still more pervasive with the increase of communicating devices used in cyber-physical environments. A prominent approach to communication between distributed devices in highly dynamic IoT environments is the use of publish-subscribe protocols such as the Message Queuing Telemetry Transport (MQTT) protocol. MQTT is designed to be light-weight while still being resilient to connectivity loss and component failures. We have developed a Coloured Petri Net model of the MQTT protocol logic using CPN Tools. The model covers all three quality of service levels provided by MQTT (at most once, at least once, and exactly once). For the verification of the protocol model, we show how an incremental model checking approach can be used to reduce the effect of the state explosion problem. This is done by exploiting that the MQTT protocol operates in phases comprised of connect, subscribe, publish, unsubscribe, and disconnect.
Alejandro Rodríguez, Lars Michael Kristensen, Adrian Rutle

Kleene Theorems for Free Choice Automata over Distributed Alphabets

We provided (PNSE’2014) expressions for free choice nets having distributed choice property which makes the nets direct product representable. In a recent work (PNSE’2016), we gave equivalent syntax for a larger class of free choice nets obtained by dropping distributed choice property.
In both these works, the classes of free choice nets were restricted by a product condition on the set of final markings. In this paper we do away with this restriction and give expressions for the resultant classes of nets which correspond to free choice synchronous products and Zielonka automata. For free choice nets with distributed choice property, we give an alternative characterization using properties checkable in polynomial time.
Free choice nets we consider are 1-bounded, S-coverable, and are labelled with distributed alphabets, where S-components of the associated S-cover respect the given alphabet distribution.
Ramchandra Phawade

Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems: A Geometric Approach

Recent studies investigated the problems of analysing Petri nets and synthesising them from labelled transition systems (LTS) with two labels (transitions) only. In this paper, we extend these works by providing new conditions for the synthesis of Weighted Marked Graphs (WMGs), a well-known and useful class of weighted Petri nets in which each place has at most one input and one output.
Some of these new conditions do not restrict the number of labels; the other ones consider up to 3 labels. Additional constraints are investigated: when the LTS is either finite or infinite, and either cyclic or acyclic. We show that one of these conditions, developed for 3 labels, does not extend to 4 nor to 5 labels. Also, we tackle geometrically the WMG-solvability of finite, acyclic LTS with any number of labels.
Raymond Devillers, Evgeny Erofeev, Thomas Hujsa

Evaluating Conformance Measures in Process Mining Using Conformance Propositions

Process mining sheds new light on the relationship between process models and real-life processes. Process discovery can be used to learn process models from event logs. Conformance checking is concerned with quantifying the quality of a business process model in relation to event data that was logged during the execution of the business process. There exist different categories of conformance measures. Recall, also called fitness, is concerned with quantifying how much of the behavior that was observed in the event log fits the process model. Precision is concerned with quantifying how much behavior a process model allows for that was never observed in the event log. Generalization is concerned with quantifying how well a process model generalizes to behavior that is possible in the business process but was never observed in the event log. Many recall, precision, and generalization measures have been developed throughout the years, but they are often defined in an ad-hoc manner without formally defining the desired properties up front. To address these problems, we formulate 21 conformance propositions and we use these propositions to evaluate current and existing conformance measures. The goal is to trigger a discussion by clearly formulating the challenges and requirements (rather than proposing new measures). Additionally, this paper serves as an overview of the conformance checking measures that are available in the process mining area.
Anja F. Syring, Niek Tax, Wil M. P. van der Aalst

Relabelling LTS for Petri Net Synthesis via Solving Separation Problems

Petri net synthesis deals with finding an unlabelled Petri net with a reachability graph isomorphic to a given usually finite labelled transition system (LTS). If there is no solution for a synthesis problem, we use label splitting. This means that we relabel edges until the LTS becomes synthesisable. We obtain an unlabelled Petri net and a relabelling function, which together form a labelled Petri net with the original, intended behaviour. By careful selection of the edges to relabel we hope to keep the alphabet of the LTS and the constructed Petri net as small as possible. Even approximation algorithms, not yielding an optimal relabelling, are hard to come by. Using region theory, we develop a polynomial heuristic based on two kinds of separation problems. These either demand distinct Petri net markings for distinct LTS states or a correspondence between the existence of an edge in the LTS and the activation of a transition under the state’s marking. If any separation problem is not solvable, relabelling of edges in the LTS becomes necessary. We show efficient ways to choose those edges.
Uli Schlachter, Harro Wimmel


Additional information