Transactions on Petri Nets and Other Models of Concurrency XV

herausgegeben von: Prof. Maciej Koutny, Fabrice Kordon, Prof. Lucia Pomello

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

The 15th volume of ToPNoC contains revised and extended versions of a selection of the best workshop and tutorial papers presented at the 40th International Conference on Application and Theory of Petri Nets and Concurrency, Petri Nets 2019, and the 19th International Conference on Application of Concurrency to System Design, ACSD 2019.

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

Inhaltsverzeichnis

Frontmatter

A Novel Token-Based Replay Technique to Speed Up Conformance Checking and Process Enhancement

Abstract

Token-based replay used to be the standard way to conduct conformance checking. With the uptake of more advanced techniques (e.g., alignment based), token-based replay got abandoned. However, despite decomposition approaches and heuristics to speed-up computation, the more advanced conformance checking techniques have limited scalability, especially when traces get longer and process models more complex. This paper presents an improved token-based replay approach that is much faster and scalable. Moreover, the approach provides more accurate diagnostics that avoid known problems (e.g., “token flooding”) and help to pinpoint compliance problems. The novel token-based replay technique has been implemented in the PM4Py process mining library. We will show that the replay technique outperforms state-of-the-art techniques in terms of speed and/or diagnostics.

Alessandro Berti, Wil M. P. van der Aalst

Extensible Structural Analysis of Petri Net Product Lines

Abstract

Petri nets are a popular formalism to represent concurrent systems. However, their standard form does not offer variability support to model and effectively analyse large sets of variants of a given system. For this purpose, we propose a notion of product line of Petri nets to represent a set of similar concurrent systems. The formalization enriches Petri nets with a feature model characterizing the variability of the systems. Moreover, places, transitions and arcs can define presence conditions that determine the subset of system variants they belong to.

To enable an efficient analysis of the set of all net variants, we have lifted several structural analysis methods for Petri nets, to the product line level. Currently, we support the lifted checking of the marked graph, state-machine, and (extended) free-choice properties, which avoids their analysis on each particular net of the product line in isolation.

We demonstrate the feasibility of our proposal using examples in the domain of flexible assembly lines, and introduce an extensible tool infrastructure. The tool is based on Eclipse and FeatureIDE, and permits adding new analysis methods externally. Moreover, we present an evaluation that shows the efficiency gains of our method with respect to an enumerative approach that analyses the properties on every net within the product line separately.

Elena Gómez-Martínez, Juan de Lara, Esther Guerra

Stability of Regional Orthomodular Posets Under Synchronisation and Refinement

Abstract

The regions of a condition/event transition system can be used to identify the sequential components of the distributed system it represents. With the aim of analysing such a system with respect to its local states, we study the structure obtained from ordering the regions by set inclusion. The resulting algebraic structure is an orthomodular partial order (omp). Given an omp, one can then define another condition/event transition system, canonical with respect to it. We are interested in characterising cases in which an omp is stable, i.e. it is isomorphic to the omp obtained as the regional structure of its canonical transition system. We propose, to this aim, a composition operation, and a refinement operation for stable orthomodular partial orders, the results of which are stable.

Federica Adobbati, Carlo Ferigato, Stefano Gandelli, Adrián Puerto Aubel

Efficient Synthesis of Weighted Marked Graphs with Circular Reachability Graph, and Beyond

Abstract

In previous studies, several methods have been developed to synthesise Petri nets from labelled transition systems (LTS), often with structural constraints on the net and on the LTS. In this paper, we focus on Weighted Marked Graphs (WMGs) and Choice-Free (CF) Petri nets, two weighted subclasses of nets in which each place has at most one output; WMGs have the additional constraint that each place has at most one input.

We provide new conditions for checking the existence of a WMG whose reachability graph is isomorphic to a given circular LTS, i.e. forming a single cycle; we develop two new polynomial-time synthesis algorithms dedicated to these constraints: the first one is LTS-based (classical synthesis) while the second one is vector-based (weak synthesis) and more efficient in general. We show that our conditions also apply to CF synthesis in the case of three-letter alphabets, and we discuss the difficulties in extending them to CF synthesis over arbitrary alphabets.

Raymond Devillers, Evgeny Erofeev, Thomas Hujsa

The Complexity of Synthesizing -Equipped Boolean Petri Nets from g-Bounded Inputs

Abstract

Boolean Petri nets equipped with \(\textsf {nop}\) allow places and transitions to be independent by being related by \(\textsf {nop}\). We characterize for any fixed \(g\in \mathbb {N}\) the computational complexity of synthesizing \(\textsf {nop}\)-equipped Boolean Petri nets from labeled directed graphs whose states have at most g incoming and at most g outgoing arcs.

Ronny Tredup

A Two-Player Asynchronous Game on Fully Observable Petri Nets

Abstract

A Petri net is distributed if its elements can be assigned to a set of locations so that each element belongs to exactly one location, and each transition belongs to the same location as its input places.

We define an asynchronous game played on the unfolding of a distributed net with two locations, the ‘user’ and the ‘environment’. The user can control the transitions in its location. A play in the game is a run in the unfolding, together with a sequence of cuts in that run. The rules of the game require that the environment satisfies a progress constraint: no transition in its location can be indefinitely postponed. In the general case, the game can be defined so that the user can observe only some transitions. In this paper, we only consider the case in which all transitions are observable, and study a reachability problem, in which the user tries to fire a target transition. We propose an algorithm which decides if the user has a winning strategy and, if so, computes a winning strategy.

Federica Adobbati, Luca Bernardinello, Lucia Pomello

Solving Finite-Linear-Path CTL-Formulas Using the CEGAR Approach

Abstract

Petri nets are an established formal method for modelling and verifying asynchronous, concurrent and distributed systems. To verify a specification, given as a temporal logic formula, state space methods often encounter the state space explosion problem. We propose a verification technique to solve the CTL query E (\( \phi \) U \( \psi \)) using the Petri net state equation with a counterexample guided abstraction refinement (CEGAR) approach. As a side product we show that (EX)\(^{k}\phi \) formulas can be solved with the CEGAR approach as well. We use these special formulas as building bricks to solve the class of finite-linear-path CTL-formulas. The proposed techniques are strong at invalidating infeasible behaviour. In addition to this it will often terminate quickly. We are also introducing quick-checks for solving EG \(\phi \) under certain circumstances.

Torsten Liebke, Karsten Wolf

Verification of the MQTT IoT Protocol Using Property-Specific CTL Sweep-Line Algorithms

Abstract

MQTT is a publish-subscribe communication protocol being increasingly used for implementing internet-of-things (IoT) applications. In earlier work we have developed a formal and executable model of the MQTT protocol using Coloured Petri Nets (CPNs) and performed an initial verification of behavioural properties. The contribution of this paper is to investigate the use of the sweep-line method for verification of the MQTT CPN model in order to alleviate the effect of the state explosion problem. We formulate the behavioural properties using Computation Tree Logic (CTL) and show how to formulate a progress measure for the sweep-line method based on the main phases of the MQTT protocol. To perform the verification of properties, we provide some property-specific CTL model checking algorithms compatible with the sweep-line method.

Alejandro Rodríguez, Lars Michael Kristensen, Adrian Rutle

Correction to: Transactions on Petri Nets and Other Models of Concurrency XV

Maciej Koutny, Fabrice Kordon, Lucia Pomello

Backmatter

Titel: Transactions on Petri Nets and Other Models of Concurrency XV
herausgegeben von: Prof. Maciej Koutny
Fabrice Kordon
Prof. Lucia Pomello
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-662-63079-2
Print ISBN: 978-3-662-63078-5
DOI: https://doi.org/10.1007/978-3-662-63079-2