Skip to main content

About this book

The 12th volume of ToPNoC contains revised and extended versions of a selection of the best workshop papers presented at the 37th International Conference on Application and Theory of Petri Nets and Concurrency, Petri Nets 2016, and the 16th International Conference on Application of Concurrency to System Design, ACSD 2016. It also contains one paper submitted directly to ToPNoC.

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: security, 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


Properties of Plain, Pure, and Safe Petri Nets

A set of necessary conditions for a Petri net to be plain, pure and safe is given. Some applications of these conditions both in practice (for Petri net synthesis), and in theory (e.g., as part of a characterisation of the reachability graphs of live and safe marked graphs) are described.
Kamila Barylska, Eike Best, Uli Schlachter, Valentin Spreckels

Similarity-Based Approaches for Determining the Number of Trace Clusters in Process Discovery

Given the complexity of real-life event logs, several trace clustering techniques have been proposed to partition an event log into subsets with a lower degree of variation. In general, these techniques assume that the number of clusters is known in advance. However, this will rarely be the case in practice. Therefore, this paper presents approaches to determine the appropriate number of clusters in a trace clustering context. In order to fulfil the objective of identifying the most appropriate number of trace clusters, two approaches built on similarity are proposed: a stability- and a separation-based method. The stability-based method iteratively calculates the similarity between clustered versions of perturbed and unperturbed event logs. Alternatively, an approach based on between-cluster dissimilarity, or separation, is proposed. Regarding practical validation, both approaches are tested on multiple real-life datasets to investigate the complementarity of the different components. Our results suggest that both methods are successful in identifying an appropriate number of trace clusters.
Pieter De Koninck, Jochen De Weerdt

Log- and Model-Based Techniques for Security-Sensitive Tackling of Obstructed Workflow Executions

Imposing access control onto workflows considerably reduces the set of users authorized to execute the workflow tasks. Further constraints (e.g. Separation of Duties) as well as unexpected unavailability of users may finally obstruct the successful workflow execution. To still complete the execution of an obstructed workflow, we envisage a hybrid approach. We first flatten the workflow and its authorizations into a Petri net and analyse for or encode the obstruction with a corresponding “obstruction marking”. If a log is provided, we partition its traces into “successful” or “obstructed” by replaying the log on the flattened net. An obstruction should then be solved by finding its nearest match from the list of successful traces. If no log is provided, the structural theory of Petri nets shall be used to provide a minimized Parikh vector, that may violate given firing rules, but reach a complete marking and by that, complete the workflow.
Julius Holderer, Josep Carmona, Farbod Taymouri, Günter Müller

Formal Modelling and Analysis of Distributed Storage Systems

Distributed storage systems are nowadays ubiquitous, very often under the form of a hierarchy of multiple caches. While a lot of effort has been dedicated to design, implement and optimise such systems, there exists to the best of our knowledge no attempt to use formal modelling and analysis in this field. This paper proposes a formal modelling framework to design distributed storage systems, with the innovating feature to separate the various concerns they involve like data-model, operations, policy, consistency, topology, etc. A model can then be analysed through model-checking to prove properties, or through simulation to assess its performance. In this paper, we define the framework and focus on performance analysis. We illustrate this on a simple yet realistic example, a LRU cache (least recently used, possibly the most known cache algorithm), showing that our proposal has the potential to be used to make design decisions before the real system is implemented.
Jordan de la Houssaye, Franck Pommereau, Philippe Deniel

DB-Nets: On the Marriage of Colored Petri Nets and Relational Databases

The integrated management of business processes and master data is being increasingly considered as a fundamental problem, by both the academia and the industry. In this position paper, we focus on the foundations of the problem, arguing that contemporary approaches struggle to find a suitable equilibrium between data- and process-related aspects. We then propose a new formal model, called db-nets, that balances such two pillars through the marriage of colored Petri nets and relational databases. We invite the research community to build on this new model, discussing in particular its potential in conceptual modeling, formal verification, and simulation.
Marco Montali, Andrey Rivkin

Transition Systems Reduction: Balancing Between Precision and Simplicity

Transition systems are a powerful formalism, which is widely used for process model representation. A number of approaches were proposed in the process mining field to tackle the problem of constructing transition systems from event logs. Existing approaches discover transition systems that are either too large or too small. In this paper we propose an original approach to discover transition systems that perfectly fit event logs and whose size is adjustable depending on the user’s need. The proposed approach allows the ability to achieve a required balance between simple and precise models.
Sergey A. Shershakov, Anna A. Kalenkova, Irina A. Lomazova

Stubborn Set Intuition Explained

This study focuses on the differences between stubborn sets and other partial order methods. First a major problem with step graphs is pointed out with an example. Then the deadlock-preserving stubborn set method is compared to the deadlock-preserving ample set and persistent set methods. Next, conditions are discussed whose purpose is to ensure that the reduced state space preserves the ordering of visible transitions, that is, transitions that may change the truth values of the propositions that the formula under verification has been built from. Finally solutions to the ignoring problem are analysed both when the purpose is to preserve only safety properties and when also liveness properties are of interest.
Antti Valmari, Henri Hansen

Decomposed Replay Using Hiding and Reduction as Abstraction

In the area of process mining, decomposed replay has been proposed to be able to deal with nets and logs containing many different activities. The main assumption behind this decomposition is that replaying many subnets and sublogs containing only some activities is faster then replaying a single net and log containing many activities. Although for many nets and logs this assumption does hold, there are also nets and logs for which it does not hold. This paper shows an example net and log for which the decomposed replay may take way more time, and provides an explanation why this is the case. Next, to mitigate this problem, this paper proposes an alternative way to abstract the subnets from the single net, and shows that the decomposed replay using this alternative abstraction is faster than the monolithic replay even for the problematic cases as identified earlier. However, the alternative abstraction often results in longer computation times for the decomposed replay than the original abstraction. An advantage of the alternative abstraction over the original abstraction is that its cost estimates are typically better.
H. M. W. Verbeek

Multiplicative Transition Systems

The paper is concerned with algebras whose elements can be used to represent runs of a system. These algebras, called multiplicative transition systems, are partial categories with respect to a partial binary operation called multiplication. They can be characterized by axioms such that their elements and operations can be represented by partially ordered multisets of a certain type and operations on such multisets. The representation can be obtained without assuming a discrete nature of represented elements. In particular, it remains valid for systems with elements which can represent continuous and partially continuous runs.
Józef Winkowski


Additional information

Premium Partner

    Image Credits