Transactions on Petri Nets and Other Models of Concurrency XI

Pragmatics Annotated Coloured Petri Nets (PA-CPNs) are a restricted class of Coloured Petri Nets (CPNs) developed to support automated generation of protocol software. The practical application of PA-CPNs and the supporting PetriCode software tool have been discussed and evaluated in earlier papers already. The contribution of this paper is to give a formal definition of PA-CPNs, motivate the definitions, and demonstrate how the structure of PA-CPNs can be exploited for more efficient verification.

How to flexibly manage complex applications over heterogeneous clouds is one of the emerging problems in the cloud era. The OASIS Topology and Orchestration Specification for Cloud Applications (TOSCA) aims at solving this problem by providing a language to describe and manage complex cloud applications in a portable, vendor-agnostic way. TOSCA permits to define an application as an orchestration of nodes, whose types can specify states, requirements, capabilities and management operations — but not how they interact each another. In this paper we first propose how to extend TOSCA to specify the behaviour of management operations and their relations with states, requirements, and capabilities. We then illustrate how such behaviour can be naturally modelled, in a compositional way, by means of open Petri nets. The proposed modelling permits to automate different analyses, such as determining whether a deployment plan is valid, which are its effects, or which plans allow to reach certain system configurations.

We introduce two families of relations on the transitions of a Petri net. The first one is an adaptation of the “reveals” relation previously defined on occurrence nets for fault diagnosis applications. Here, this relation is considered for modeling positive information flow, which arises when the occurrence of a transition gives the information that another transition already occurred or will occur. The second one, called “excludes”, is presented for modeling negative information flow, which arises when the occurrence of a transition gives information on the non-occurrence of another transition, in the past or in the future. We consider the notion of non-interference proposed in the literature for formalizing security in distributed systems. On the basis of reveals and excludes relations we propose a collection of new notions of non-interference for ordinary Petri nets and compare them with notions already proposed in the literature.

This paper investigates the feature negotiation procedure of the Datagram Congestion Control Protocol (DCCP) in RFC 4340 using Coloured Petri Nets (CPNs). After obtaining a formal executable CPN model of DCCP feature negotiation, we analyse it using state spaces. The experimental result reveals that simultaneous negotiation may be incorrect and broken on even a lossless FIFO channel. In the undesired terminal states, the confirmed feature values of the client and the server do not match. To fix this problem we suggest two solutions. Firstly, sending a Change option when an endpoint changes its preference. Secondly, an endpoint in STABLE does not discard non-reordered Confirm options. We have applied our suggested changes to the constructed CPN models. The formal verification of the revised models shows that the undesired terminal states have been eliminated.

This paper presents an approach to the development of modeling languages and automated generation of specific modeling tools based on meta-models. Modeling is one of the main tasks in engineering. Graphical modeling helps the engineer not only to understand the system but also to communicate with engineers and with other stakeholders that participate in the development (or analytic) process.

In order to be able to provide adequately adapted modeling techniques for a given domain, it is useful to support the development of techniques that are designed for their special purpose, i.e. domain-specific modeling languages (DSML). For this purpose meta-modeling comes in handy. Meta-models provide a clear abstract syntax and model-driven design approaches allow for rapid prototyping of modeling languages. However, the transformation and also the original (source model) as well as the transformed (target) model often do not provide a clear semantics.

We present an approach to model-driven development that is based on Petri nets: high- and low-level Petri nets in various formalisms can be used as target models. The presented approach uses ontology-based meta-models, code and graphical templates, as well as custom and predefined transformation engines. The RMT framework provides the generation of modeling tools and the transformation into executable and/or analyzable models based on the defined Petri net semantics.

Process mining techniques rely on event logs: the extraction of a process model (discovery) takes an event log as the input, the adequacy of a process model (conformance) is checked against an event log, and the enhancement of a process model is performed by using available data in the log. Several notations and formalisms for event log representation have been proposed in the recent years to enable efficient algorithms for the aforementioned process mining problems. In this paper we show how Conditional Partial Order Graphs (CPOGs), a recently introduced formalism for compact representation of families of partial orders, can be used in the process mining field, in particular for addressing the problem of compact and easy-to-comprehend representation of event logs with data. We present algorithms for extracting both the control flow as well as the relevant data parameters from a given event log and show how CPOGs can be used for efficient and effective visualisation of the obtained results. We demonstrate that the resulting representation can be used to reveal the hidden interplay between the control and data flows of a process, thereby opening way for new process mining techniques capable of exploiting this interplay. Finally, we present open-source software support and discuss current limitations of the proposed approach.

A word is called Petri net solvable if it is isomorphic to the reachability graph of an unlabelled Petri net. In this paper, the class of finite, two-letter, Petri net solvable, words is studied. Two conjectures providing different characterisations of this class of words are motivated and proposed. One conjecture characterises the class in terms of pattern-matching, the other in terms of letter-counting. Several results are described which amount to a partial proof of these conjectures.

Given a log L, a control-flow discovery algorithm f, and a quality metric m, this paper faces the following problem: what are the parameters in f that mostly influence its application in terms of m when applied to L? This paper proposes a method to face this problem, based on sensitivity analysis, a theory which has been successfully applied in other areas. Clearly, a satisfactory solution to this problem will be crucial to bridge the gap between process discovery algorithms and final users. Additionally, recommendation techniques and meta-techniques like determining the representational bias of an algorithm may benefit from solutions to the problem considered in this paper. The method has been evaluated over a set of logs and two different miners: the inductive miner and the flexible heuristic miner, and the experimental results witness the applicability of the general framework described in this paper.

Negotiations have recently been introduced as a model of concurrency with multi-party negotiation atoms as primitive. This paper studies the relation between negotiations and Petri nets. In particular, we show that each negotiation can be translated into a 1-safe labelled Petri net with equivalent behaviour. In the general case, this Petri net is exponentially larger than the negotiation. For deterministic negotiations, however, the corresponding Petri has linear size compared to the negotiation, and it enjoys the free-choice property. We show that for this class the negotiation is sound if and only if the corresponding Petri net is sound. Finally, we have a look at the converse direction: given a Petri net, can we find a corresponding negotiation?

Business process models expressed in languages such as BPMN (Business Process Model and Notation), play a critical role in implementing the workflows in modern enterprises. However, control flow errors such as deadlocks and lack of synchronization, and syntactic errors arising out of poor modeling practices often occur in industrial process models. A major challenge is to provide the means and methods to detect such errors and more importantly, to identify the location of each error. In this work, we develop a formal framework of diagnosing errors by locating their occurrence nodes in business process models at the level of sub-processes and swim-lanes. We use graph-theoretic techniques and Petri net-based analyses to detect syntactic and control flow-related errors respectively. While syntactic errors can be easily located on the processes themselves, we project control-related errors on processes using a mapping from Petri nets to processes. We use this framework to analyze a sample of 174 industrial BPMN process models having 1262 sub-processes in which we identify more than 2000 errors. We are further able to discover how error frequencies change with error depth, how they correlate with the size of the sub-processes and swim-lane interactions in the models, and how they can be predicted in terms of process metrics like sub-process size, coefficient of connectivity, sequentiality and structuredness.

The Model Checking Contest (MCC) is an annual competition between software tools that verify concurrent systems using state-space exploration techniques, either explicit-state or symbolic. The present article provides a comprehensive account of the 2015 edition of the MCC. The principles of the contest are described, together with its underlying software infrastructure. The tools that competed in 2015 are listed and the results of the contest are summarized.

We report on the performance of the tool LoLA 2.0 in the model checking contest (MCC) 2015. As in the years before, LoLA ranked first in the reachability category of the contest. We identify critical success factors and discuss the impact of the contest design. Conclusions include further improvements for the tool as well as suggestions concerning the setup of future contests.

MARCIE is a Petri net analysis tool supporting qualitative and quantitative analyses including model checking facilities. Particular features are symbolic state space analysis including efficient saturation-based state space generation, evaluation of standard Petri net properties, and CTL model checking. Most of MARCIE’s features build on Interval Decision Diagrams (IDDs) to efficiently encode interval logic functions representing marking sets of bounded Petri nets. This allows the efficient support of qualitative state space based analysis techniques. Among others, MARCIE applies heuristics for the computation of static variable orders to obtain concise IDD representations. In this paper we focus on those aspects which are crucial for MARCIE’s regular success in the annual Model Checking Contest of the Petri net community.

Symbolic model checking with decision diagrams is a very efficient technique for handling large models. However, even when using advanced algorithms, model checking tools still need to be carefully written. Indeed, they are both CPU and memory bounded: in addition to the algorithms complexity, the limiting factors are the available memory and how fast computations are performed. Thus, each saved CPU cycle or byte can make the difference between a successful model checker and a failing one.

We present pnmc, a symbolic model checker for Petri Nets, and libsdd, its associated library which implements Hierarchical Set Decision Diagrams and automatic saturation. Reliability aside, choices were always made to favour performance.

The combination of advanced algorithms for symbolic model checking and advanced coding techniques offer very good results as shown in the Model Checking Contest 2015, which is used as a background to present pnmc and libsdd.

We discuss selected model checking techniques used in the tool TAPAAL for the reachability analysis of weighted Petri nets with inhibitor arcs. We focus on techniques that had the most significant effect at the 2015 Model Checking Contest (MCC). While the techniques are mostly well known, our contribution lies in their adaptation to the MCC reachability queries, their efficient implementation and the evaluation of their performance on a large variety of nets from MCC’15.