Skip to main content
main-content

Über dieses Buch

This book constitutes the proceedings of the 39th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2018, held in Bratislava, Slovakia, in June 2018. Petri Nets 2017 is co-located with the 19th International Conference on Application of Concurrency to System Design, ACSD 2018.

The 15 regular and 8 tool papers, with 1 invited talk presented together in this volume were carefully reviewed and selected from 33 submissions. The focus of the conference is on following topics: Petri Nets Synthesis; Analysis and Model Checking; Languages; Semantics and Expressiveness; and Tools.

Inhaltsverzeichnis

Frontmatter

Invited Talk

Frontmatter

Self-adaptive Model Checking, the Next Step?

Abstract
Model checking is becoming a popular verification method that still suffers from combinatorial explosion when used on large industrial systems. Currently, experts can, in some cases, overcome this complexity by selecting appropriate modeling and verification techniques, as well as an adapted representation of the system. Unfortunately, this cannot yet be done automatically, thus hindering the use of model checking in industry.
The objective of this paper is to sketch a way to tackle this problem by introducing self-adaptive model checking. This is a long term goal that could lead the community to elaborate a new generation of model checkers able to successfully push forwards the scale of the systems they can deal with.
Fabrice Kordon, Yann Thierry-Mieg

Petri Net Synthesis

Frontmatter

Analysis and Synthesis of Weighted Marked Graph Petri Nets

Abstract
Numerous real-world systems can be modeled with Petri nets, which allow a combination of concurrency with synchronizations and conflicts. To alleviate the difficulty of checking their behaviour, a common approach consists in studying specific subclasses. In the converse problem of Petri net synthesis, a Petri net of some subclass has to be constructed efficiently from a given specification, typically from a labelled transition system describing the behaviour of the desired net.
In this paper, we focus on a notorious subclass of persistent Petri nets, the weighted marked graphs (WMGs), also called generalised (or weighted) event (or marked) graphs or weighted T-nets. In such nets, edges have multiplicities (weights) and each place has at most one ingoing and one outgoing transition. Although extensively studied in previous works and benefiting from strong results, both their analysis and synthesis can be further investigated. To this end, we provide new conditions delineating more precisely their behaviour and give a dedicated synthesis procedure.
Raymond Devillers, Thomas Hujsa

Elementary Net Synthesis Remains NP-Complete Even for Extremely Simple Inputs

Abstract
Elementary net systems (ENS) are the most fundamental class of Petri nets. Their synthesis problem has important applications in the design of digital hardware and commercial processes. Given a labeled transition system (TS) A, feasibility is the NP-complete decision problem whether A can be synthesized into an ENS. It is known that A is feasible if and only if it has the event state separation property (ESSP) and the state separation property (SSP). Recently, these properties have also been studied individually for their practical implications. A fast ESSP algorithm, for instance, would allow applications to at least validate the language equivalence of A and a synthesized ENS. Being able to efficiently decide SSP, on the other hand, could serve as a quick-fail preprocessing mechanism for synthesis. Although a few tractable subclasses have been found, this paper destroys much of the hope that many practically meaningful input restrictions make feasibility or at least one of ESSP and SSP efficient. We show that all three problems remain NP-complete even if the input is restricted to linear TSs where every event occurs at most three times.
Ronny Tredup, Christian Rosenke, Karsten Wolf

Petri Net Synthesis with Union/Find

Abstract
We propose a new algorithm for the synthesis of a Petri net from a transition system. It is presented for a class of place/transition Petri nets we call \(\varDelta \)1-Petri nets. A \(\varDelta \)1-Petri net has an incidence matrix where entries have values 0, 1, and −1 only. This class includes safe Petri nets as well as ordinary place/transition nets. The proposed algorithm can be adapted to these net classes. The algorithm employs Tarjan’s union/find algorithm for managing sets of vertices. It requires just O(|V||T|) space where V is the set of vertices and T is the set of transition labels. Consequently, problem instances even beyond 1,000,000 vertices have a manageable memory footprint. Our results are experimentally validated using a prototype implementation.
Karsten Wolf

Factorisation of Petri Net Solvable Transition Systems

Abstract
In recent papers, general conditions were developed to characterise when and how a labelled transition system may be factorised into non-trivial factors. These conditions combine a local property (strong diamonds) and a global one (separation), the latter being of course more delicate to check. Since one of the aims of such a factorisation was to speed up the synthesis of Petri nets from such labelled transition systems, the problem arises to analyse if those conditions (and in particular the global one) could be simplified, or even dropped, in the special case of Petri net solvable behaviours, i.e., when Petri net synthesis is possible. This will be the subject of the present paper.
Raymond Devillers, Uli Schlachter

A Geometric Characterisation of Event/State Separation

Abstract
Region theory, as initiated by Ehrenfeucht and Rozenberg, allows the characterisation of the class of Petri net synthesisable finite labelled transition systems. Two kinds of problems need to be solved for such a synthesis, state separation problems for distinguishing states and event/state separation problems for preventing unwanted behaviour. In the present paper, the class of finite labelled transition systems in which all event/state separation problems are solvable shall be characterised geometrically, rather than linear-algebraically.
Uli Schlachter, Harro Wimmel

From Event-Oriented Models to Transition Systems

Abstract
Two structurally different methods of associating transition system semantics to event-oriented models of distributed systems are distinguished in the literature. One of them is based on configurations (event sets), the other on residuals (model fragments). In this paper, a variety of models is investigated, ranging from extended prime event structures to configuration structures, and it is shown that the two semantics lead to isomorphic results. This strengthens prior work where bisimilarity (but not necessarily isomorphism) is achieved for a smaller range of models. Thanks to the isomorphisms obtained here, a wide range of facts known from the literature on configuration-based transition systems can be extended to residual-based ones.
Eike Best, Nataliya Gribovskaya, Irina Virbitskaite

Analysis and Model Checking

Frontmatter

Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

Abstract
We study techniques to overcome the state space explosion problem in CTL model checking of Petri nets. Classical state space pruning approaches like partial order reductions and structural reductions become less efficient with the growing size of the CTL formula. The reason is that the more places and transitions are used as atomic propositions in a given formula, the more of the behaviour (interleaving) becomes relevant for the validity of the formula. We suggest several methods to reduce the size of CTL formulae, while preserving their validity. By these methods, we significantly increase the benefits of structural and partial order reductions, as the combination of our techniques can achive up to 60% average reduction in formulae sizes. The algorithms are implemented in the open-source verification tool TAPAAL and we document the efficiency of our approach on a large benchmark of Petri net models and queries from the Model Checking Contest 2017.
Frederik Bønneland, Jakob Dyhr, Peter G. Jensen, Mads Johannsen, Jiří Srba

Basis Coverability Graph for Partially Observable Petri Nets with Application to Diagnosability Analysis

Abstract
Petri nets have been proposed as a fundamental model for discrete-event systems in a wide variety of applications and have been an asset to reduce the computational complexity involved in solving a series of problems, such as control, state estimation, fault diagnosis, etc. Many of those problems require an analysis of the reachability graph of the Petri net. The basis reachability graph is a condensed version of the reachability graph that was introduced to efficiently solve problems linked to partial observation. It was in particular used for diagnosis which consists in deciding whether some fault events occurred or not in the system, given partial observations on the run of the system. However this method is, with very specific exceptions, limited to bounded Petri nets. In this paper, we introduce the notion of basis coverability graph to remove this requirement. We then establish the relationship between the coverability graph and the basis coverability graph. Finally, we focus on the diagnosability problem: we show how the basis coverability graph can be used to get an efficient algorithm.
Engel Lefaucheux, Alessandro Giua, Carla Seatzu

Co-finiteness and Co-emptiness of Reachability Sets in Vector Addition Systems with States

Abstract
The coverability and boundedness problems are well-known exponential-space complete problems for vector addition systems with states (or Petri nets). The boundedness problem asks if the reachability set (for a given initial configuration) is finite. Here we consider a dual problem, the co-finiteness problem that asks if the complement of the reachability set is finite; by restricting the question we get the co-emptiness (or universality) problem that asks if all configurations are reachable.
We show that both the co-finiteness problem and the co-emptiness problem are complete for exponential space. While the lower bounds are obtained by a straightforward reduction from coverability, getting the upper bounds is more involved; in particular we use the bounds derived for reversible reachability by Leroux in 2013.
The studied problems have been motivated by a recent result for structural liveness of Petri nets; this problem has been shown decidable by Jančar in 2017 but its complexity has not been clarified. The problem is tightly related to a generalization of the co-emptiness problem for non-singleton sets of initial markings, in particular for downward closed sets. We formulate the problems generally for semilinear sets of initial markings, and in this case we show that the co-emptiness problem is decidable (without giving an upper complexity bound) and we formulate a conjecture under which the co-finiteness problem is also decidable.
Petr Jančar, Jérôme Leroux, Grégoire Sutre

Languages

Frontmatter

An Efficient Characterization of Petri Net Solvable Binary Words

Abstract
We present a simple characterization of the set of Petri net solvable binary words. It states that they are exactly the extensions of the prefixes of Petri net cyclic solvable words, by some prefix \(x^k\), where x is any letter of the binary alphabet being considered, and k is any natural number. We derive several consequences of this characterization which, in a way, shows that the set of solvable words is ‘smaller than expected’. Therefore, the existing conjecture that all of them can be generated by quite simple net is not only confirmed, but indeed reinforced. As a byproduct of the characterization, we also present a linear time algorithm for deciding whether a binary word is solvable. The key idea is that the connection with the cyclic solvable words induces certain structural regularity. Therefore, one just needs to look for possible irregularities, which can be done in a structural way, resulting in a rather surprising linearity of the decision algorithm. Finally, we employ the obtained results to provide a characterization of reversible binary transition systems.
David de Frutos Escrig, Maciej Koutny, Łukasz Mikulski

Pattern Matching in Link Streams: A Token-Based Approach

Abstract
Link streams model the dynamics of interactions in complex distributed systems as sequences of links (interactions) occurring at a given time. Detecting patterns in such sequences is crucial for many applications but it raises several challenges. In particular, there is no generic approach for the specification and detection of link stream patterns in a way similar to regular expressions and automata for text patterns. To address this, we propose a novel automata framework integrating both timed constraints and finite memory together with a recognition algorithm. The algorithm uses structures similar to tokens in high-level Petri nets and includes non-determinism and concurrency. We illustrate the use of our framework in real-world cases and evaluate its practical performances.
Clément Bertrand, Hanna Klaudel, Matthieu Latapy, Frédéric Peschanski

Semantics and Expressiveness

Frontmatter

Modeling Operational Semantics with Interval Orders Represented by Sequences of Antichains

Abstract
A representation of interval orders by sequences of antichains is discussed and its relationship to the Fishburn’s representation by sequences of beginnings and endings is analyzed in detail. Using sequences of antichains to model operational semantics of elementary inhibitor nets is also discussed.
Ryszard Janicki

One Net Fits All

A Unifying Semantics of Dynamic Fault Trees Using GSPNs
Abstract
Dynamic Fault Trees (DFTs) are a prominent model in reliability engineering. They are strictly more expressive than static fault trees, but this comes at a price: their interpretation is non-trivial and leaves quite some freedom. This paper presents a GSPN semantics for DFTs. This semantics is rather simple and compositional. The key feature is that this GSPN semantics unifies all existing DFT semantics from the literature. All semantic variants can be obtained by choosing appropriate priorities and treatment of non-determinism.
Sebastian Junges, Joost-Pieter Katoen, Mariëlle Stoelinga, Matthias Volk

On the Structure of Cycloids Introduced by Carl Adam Petri

Abstract
Cycloids are particular Petri nets for modelling processes of actions or events. They belong to the fundaments of Petri’s general systems theory and have very different interpretations, ranging from Einstein’s relativity theory to elementary information processing gates. Despite their simple definitions, their properties are still not completely understood. This contribution provides for the first time a formal definition together with new results concerning their structure. For instance, it is shown that the minimal length of a cycle is the length of a local basic circuit, possibly decreased by an integer multiple of the number of semi-active transitions.
Rüdiger Valk

Markings in Perpetual Free-Choice Nets Are Fully Characterized by Their Enabled Transitions

Abstract
A marked Petri net is lucent if there are no two different reachable markings enabling the same set of transitions, i.e., states are fully characterized by the transitions they enable. This paper explores the class of marked Petri nets that are lucent and proves that perpetual marked free-choice nets are lucent. Perpetual free-choice nets are free-choice Petri nets that are live and bounded and have a home cluster, i.e., there is a cluster such that from any reachable state there is a reachable state marking the places of this cluster. A home cluster in a perpetual net serves as a “regeneration point” of the process, e.g., to start a new process instance (case, job, cycle, etc.). Many “well-behaved” process models fall into this class. For example, the class of short-circuited sound workflow nets is perpetual. Also, the class of processes satisfying the conditions of the \(\alpha \) algorithm for process discovery falls into this category. This paper shows that the states in a perpetual marked free-choice net are fully characterized by the transitions they enable, i.e., these process models are lucent. Having a one-to-one correspondence between the actions that can happen and the state of the process, is valuable in a variety of application domains. The full characterization of markings in terms of enabled transitions makes perpetual free-choice nets interesting for workflow analysis and process mining. In fact, we anticipate new verification, process discovery, and conformance checking techniques for the subclasses identified.
Wil M. P. van der Aalst

Tools

Frontmatter

ePNK Applications and Annotations: A Simulator for YAWL Nets

Abstract
The ePNK is an Eclipse based platform and framework for developing and integrating Petri net tools and applications. New types of Petri nets can be realized and plugged into the ePNK without any programming by simply providing a model of the concepts of the new Petri net type. Moreover, the ePNK allows developers to customize the graphical appearance of the features of a new Petri net type.
In this paper, we discuss how to implement applications for the ePNK, and how they can interact with the end user by so-called annotations. This is discussed by the example of a simulator for YAWL nets.
Ekkart Kindler

Petri Net Model Checking with LoLA 2

Abstract
LoLA 2 offers a suite of algorithms for verifying place/transition Petri nets. It combines structural with state space methods and general purpose with Petri net-specific techniques. The methods are easily accessible to people with little knowledge of Petri nets since there is a uniform query language based on temporal logic, and the tool takes care of sound application of its methods. Unlike its predecessor LoLA 1, LoLA 2 is based on a strict modularisation and integration of various standard tools. A careful software engineering approach has been used for coding. Through its code quality and its frequent comparison to other tools in the yearly model checking contests, LoLA 2 has become one of the most reliable verification tools for distributed systems.
Karsten Wolf

Integrating Simulink Models into the Model Checker Cosmos

Abstract
We present an implementation for Simulink model executions in the statistical model-checker Cosmos. We take profit of this implementation for hybrid modeling and simulations combining Petri nets and Simulink models.
Benoît Barbot, Béatrice Bérard, Yann Duplouy, Serge Haddad

LocalProcessModelDiscovery: Bringing Petri Nets to the Pattern Mining World

Abstract
This paper introduces the tool LocalProcessModelDiscovery, which is available as a package in the process mining toolkit ProM. LocalProcessModelDiscovery aims to discover local process models, i.e., frequent patterns extracted from event logs, where each frequent pattern is expressed in the form of a Petri net. Local process models can be positioned in-between process discovery and Petri net synthesis on the one hand, and sequential pattern mining on the other hand. Like pattern mining techniques, the LocalProcessModelDiscovery tool focuses on the extraction of a set of frequent patterns, in contrast to Petri net synthesis and process discovery techniques that aim to describe all behavior seen in an event log in the form of a single model. Like Petri net synthesis and process discovery techniques, the models discovered with LocalProcessModelDiscovery can express a diverse set of behavioral constructs. This contrasts sequential pattern mining techniques, which are limited to patterns that describe sequential orderings in the data and are unable to express loops, choices, and concurrency.
Niek Tax, Natalia Sidorova, Wil M. P. van der Aalst, Reinder Haakma

A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning

Abstract
This paper introduces mcc4mcc, the Model Checker Collection for the Model Checking Contest, a tool that wraps multiple model checking solutions, and applies the most appropriate one based on the characteristics of the model it is given. It leverages machine learning algorithms to carry out this selection, based on the results gathered from the 2017 edition of the Model Checking Contest, an annual event in which multiple tools compete to verify different properties on a large variety of models. Our approach brings two important contributions. First, our tool offers the opportunity to further investigate on the relation between model characteristics and verification techniques. Second, it lays out the groundwork for a unified way to distribute model checking software using virtual containers.
Didier Buchs, Stefan Klikovits, Alban Linard, Romain Mencattini, Dimitri Racordon

Arduino Library Developed for Petri Net Inserted into RFID Database and Variants

Abstract
This work has the purpose of present the implementation of an innovative approach called PNRD (elementary Petri Net inside a RFID distributed Database) and its variation, the inverted PNRD. In this approach, the theoretical model widely studied and developed of Petri Nets is the base to define a data structure to be recorded in RFID tags. The tags are used as an object distributed database. The result is a highly adaptive, distributed, scalable and applicable control system. Therefore, this work describes the design, implementation, and validation of a library for the Arduino® platform which simplifies the development of new applications that uses the PNRD approach as well as the inverted PNRD.
Carlos Eduardo Alves da Silva, José Jean-Paul Zanlucchi de Souza Tavares, Marco Vinícius Muniz Ferreira

OMPetri - A Software Application for Modeling and Simulation Using Extended Hybrid Petri Nets by Employing OpenModelica

Abstract
In this paper we present OMPetri, a new tool for modeling, simulation, and analyzing of a powerful unifying Petri net concept: extended hybrid Petri nets (xHPN). The software features a modern, lightweight, and intuitive graphical user interface that focuses on users who are new to Petri nets, while also enabling experienced users to model more complex and advanced systems. It has not been designed for any specific application cases. Thus it is as universal as the related Petri net formalism that can be applied for modeling systems of various research areas, such as systems biology, business processes, and industrial workflows.
It greatly enables and simplifies the modeling of discrete, continuous, and hybrid Petri nets. New models can be created and existing models can be modified and improved quickly and easily due to two different model views. During the process of modeling, the Petri net may change its class (discrete, continuous, hybrid) and solving strategies for conflicts can be defined.
The tool employs OpenModelica and the advanced Modelica Petri net library PNlib to provide an elaborated and powerful simulation environment. Additionally, it provides basic features to check and evaluate the model and to analyze simulation results generated by the simulation back-end.
Both, the tool, as well as OpenModelica are open source and free of charge for academic usage. Java source code, executable JAR and a tutorial are available at: https://​agbi.​techfak.​uni-bielefeld.​de/​OMPetri.
Christoph Brinkrolf, Philo Reipke

GreatTeach: A Tool for Teaching (Stochastic) Petri Nets

Abstract
GreatSPN is a collection of tools for modelling and analysis of systems using (stochastic) Petri nets. It features a modern Java-based graphical interface. But being technologically advanced does not mean that the tool learning curve is significantly simplified. In the tool the simple features that are needed for educational purpose are intermixed with more advanced features that require a deeper understanding of the formalisms and of the solvers. This paper presents GreatTeach, a streamlined and enriched version of GreatSPN meant for teaching resulting from our experience in teaching Petri nets to master students.
Elvio Gilberto Amparore, Susanna Donatelli

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise