Skip to main content

About this book

The 13th volume of ToPNoC contains revised and extended versions of a selection of the best workshop papers presented at the 38th International Conference on Application and Theory of Petri Nets and Concurrency, Petri Nets 2017, and the 17th International Conference on Application of Concurrency to System Design, ACSD 2017.

The 9 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: fault-tolerance, service composition, databases, communication protocols, business processes, and distributed systems. Thus, this volume gives a good overview of ongoing research on concurrent systems and Petri nets.

Table of Contents


Computing Alignments of Event Data and Process Models

The aim of conformance checking is to assess whether a process model and event data, recorded in an event log, conform to each other. In recent years, alignments have proven extremely useful for calculating conformance statistics. Computing optimal alignments is equivalent to solving a shortest path problem on the state space of the synchronous product net of a process model and event data. State-of-the-art alignment based conformance checking implementations exploit the \(A^* \)-algorithm, a heuristic search method for shortest path problems, and include a wide range of parameters that likely influence their performance. In previous work, we presented a preliminary and exploratory analysis of the effect of these parameters. This paper extends the aforementioned work by means of large-scale statistically-sound experiments that describe the effects and trends of these parameters for different populations of process models. Our results show that, indeed, there exist parameter configurations that have a significant positive impact on alignment computation efficiency.
Sebastiaan J. van Zelst, Alfredo Bolt, Boudewijn F. van Dongen

Heuristic Mining Approaches for High-Utility Local Process Models

Local Process Models (LPMs) describe structured fragments of process behavior that occur in the context of business processes. Traditional support-based LPM discovery aims to generate a collection of process models that describe highly frequent behavior, in contrast, in High-Utility Local Process Model (HU-LPM) mining the aim is to generate a collection of process models that provide useful business insights according to a specified utility function. Mining LPMs is computationally expensive as the search space depends combinatorially on the number of activities in the business process. In support-based LPM mining, the search space is constrained by leveraging the anti-monotonic property of support (i.e., the apriori principle). We show that there is no property of monotonicity or anti-monotonicity in HU-LPM mining that allows for lossless pruning of the search space. We propose four heuristic methods to explore the search space only partially. We show on a collection of 57 event logs that these heuristics techniques can reduce the size of the search space of HU-LPM mining without much loss in the mined set of HU-LPMs. Furthermore, we analyze the effect of several properties of the event log on the performance of the heuristics through statistical analysis. Additionally, we use predictive modeling with regression trees to explore the relation between combinations of log properties and the effect of the heuristics on the size of the search space and on the quality of the HU-LPMs, where the statistical analysis focuses on the effect of log properties in isolation.
Benjamin Dalmas, Niek Tax, Sylvie Norre

On Stability of Regional Orthomodular Posets

The set of regions of a transition system, ordered by set inclusion, is an orthomodular poset, often referred to as quantum logic, here called regional logic. Regional logics, which are known to be regular and rich, are the main subject of investigation in this work. Given a regular, rich logic L, one can build a transition system A, such that L embeds into the regional logic of A. Call a logic stable if the embedding is an isomorphism. We give some necessary conditions for a logic to be stable, and show that under these, the embedding has some stronger property. In particular, we show that any \(\{0,1\}\)-pasting of n stable logics is stable, and that, whenever L contains n maximal Boolean sublogics with pairwise identical intersections, L is stable. The full characterization of the class of stable logics is still an open problem.
Luca Bernardinello, Carlo Ferigato, Lucia Pomello, Adrián Puerto Aubel

Decision Diagrams for Petri Nets: A Comparison of Variable Ordering Algorithms

The efficacy of decision diagram techniques for state space generation is known to be heavily dependent on the variable order. Ordering can be done a-priori (static) or during the state space generation (dynamic). We focus our attention on static ordering techniques. Many static decision diagram variable ordering techniques exist, but it is hard to choose which method to use, since only fragmented performance information is available. In the work reported in this paper we used the models of the Model Checking Contest 2017 edition to conduct an extensive comparison of 18 different algorithms, in order to better understand their efficacy. Comparison is based on the size of the decision diagram of the reachable state space, which is generated using the Saturation method provided by the Meddly library.
Elvio Gilberto Amparore, Susanna Donatelli, Marco Beccuti, Giulio Garbi, Andrew Miner

Model Synchronization and Concurrent Simulation of Multiple Formalisms Based on Reference Nets

Nowadays, modeling complex systems requires a combination of techniques to facilitate multiple perspectives and adequate modeling. Therefore, UML and other formalisms are used in combination with Petri nets. Often the different models are transformed into a single formalism to simulate the resulting models within a homogeneous execution environment. For UML, the mapping is usually done via the transformation to some programming language.
Anyhow, the problem with generative techniques is that the different perspectives that are provided by the applied modeling techniques can hardly be retained once the models are transformed into a single formalism. In this contribution we elaborate on how multiple formalisms can be used together in their original representation.
One of the main challenges for our approach is the provision of means for coupling mentioned formalisms so they can be executed together. We utilize the synchronization features of Reference Nets to couple multiple modeling techniques. Therefore, we present an approach to transform modeling languages into Reference Nets, which can be executed with the simulation environment Renew. The simulation events are forwarded to the original representation in the form of graphical user feedback and interaction.
This results in a simultaneous and concurrent execution of models featuring a combination of multiple modeling formalisms. A finite automata modeling and simulation tool is presented to showcase the application of our concept. Based on our results, we present a case study that utilizes finite automata in combination with Reference Nets and activity diagrams.
Pascale Möller, Michael Haustermann, David Mosteller, Dennis Schmitz

Complexity Aspects of Web Services Composition

The web service composition problem can be stated as follows: given a finite state machine M, representing a service business protocol, and a set of finite state machines \(\mathcal {R}\), representing the business protocols of existing services, the question is to check whether there is a simulation relation between M and the shuffle product closure of \(\mathcal {R}\).
This paper studies the impact of several parameters on the complexity of this problem. We show that the problem is Exptime-complete if we bound either: (i) the number of instances of services in \(\mathcal {R}\) that can be used in a composition, or(ii) the number of instances of services in \(\mathcal {R}\) that can be used in parallel, or (iii) the number of the so-called hybrid states in the finite state machines of \(\mathcal {R}\) by 0, 1 or 2. The problem is still open for 3 hybrid states.
Karima Ennaoui, Lhouari Nourine, Farouk Toumani

GPU Computations and Memory Access Model Based on Petri Nets

In modern systems CPUs as well as GPUs are equipped with multi-level memory architectures, where different levels of the hierarchy vary in latency and capacity. Therefore, various memory access models were studied. Such a model can be seen as an interface abstracting the user from the physical architecture details. In this paper we present a general and uniform GPU computation and memory access model based on bounded inhibitor Petri nets (PNs). Its effectiveness is demonstrated by comparing its throughputs to practical computational experiments performed with the usage of Nvidia GPU with CUDA architecture.
Our PN model is consistent with the workflow of multithreaded GPU streaming multiprocessors. It models a selection and execution of instructions for each warp. The three types of instructions included in the model are: the arithmetic operation, the access to the shared memory and the access to the global memory. For a given algorithm the model allows to check how efficient the parallelization is, and whether a different organization of threads will improve performance.
The accuracy of our model was tested with different kernels. As the preliminary experiments we used the matrix multiplication program and stability example created by Nvidia, and as the main experiment a binary version of the least significant digit radix sort algorithm. We created three implementations of the algorithm using CUDA architecture, differing in the usage of shared and global memory as well as organization of calculations. For each implementation the PN model was used and the results of experiments are presented in the work.
Anna Gogolińska, Łukasz Mikulski, Marcin Piątkowski

Model-Based Testing of the Gorums Framework for Fault-Tolerant Distributed Systems

Data replication is a central mechanism for the engineering of fault-tolerant distributed systems, and is used in the realization of most cloud computing services. This paper explores the use of Coloured Petri Nets (CPNs) for model-based testing of quorum-based distributed systems. We have developed an approach to model-based testing of fault-tolerant services implemented using the Go language and the Gorums framework. We show how a CPN model can be used to obtain both unit test cases for the quorum logic functions, and system level test cases consisting of quorum calls. The CPN model is also used to obtain the test oracles against which the result of running a test case can be compared. We demonstrate the application of our approach by considering an implementation of a distributed storage service on which we obtain 100% code coverage for the quorum functions, 96.7% statement coverage on the quorum calls, and 52.3% coverage on the Gorums framework. We demonstrate similar encouraging results also on a more complex Gorums-based implementation of the Paxos consensus protocol.
Rui Wang, Lars Michael Kristensen, Hein Meling, Volker Stolz

MCC’2017 – The Seventh Model Checking Contest

Created in 2011, the Model Checking Contest (MCC) is an annual competition dedicated to provide a fair evaluation of software tools that verify concurrent systems using state-space exploration techniques and model checking. This article presents the principles and results of the 2017 edition of the MCC, which took place along with the Petri Net and ACSD joint conferences in Zaragoza, Spain.
Fabrice Kordon, Hubert Garavel, Lom Messan Hillah, Emmanuel Paviot-Adet, Loïg Jezequel, Francis Hulin-Hubard, Elvio Amparore, Marco Beccuti, Bernard Berthomieu, Hugues Evrard, Peter G. Jensen, Didier Le Botlan, Torsten Liebke, Jeroen Meijer, Jiří Srba, Yann Thierry-Mieg, Jaco van de Pol, Karsten Wolf


Additional information