Transactions on Petri Nets and Other Models of Concurrency XIII

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.