Fundamenta Informaticae

Separability in Petri nets means the property for a net k · N with an initial marking k · M to behave in the same way as k parallel instances of the same net N with an initial marking M, thus divided by k. We prove the separability of plain, bounded, reversible and persistent Petri nets, a class of nets that extends the well-known live and bounded marked graphs. We establish first a weak form of separability, already known to hold for marked graphs, in which every firing sequence of k · N is simulated by a firing sequence of k parallel instances of N with an identical firing count. We establish on top of this a strong form of separability, in which every firing sequence of k · N is simulated by an identical firing sequence of k parallel instances of N.

Workflow mining is the task of automatically producing a workflow model from a set of event logs recording sequences of workflow events; each sequence corresponds to a use case or workflow instance. Formal approaches to workflow mining assume that the event log is complete (contains enough information to infer the workflow) which is often not the case. We present a learning approach that relaxes this assumption: if the event log is incomplete, our learning algorithm automatically derives queries about the executability of some event sequences. If a teacher answers these queries, the algorithm is guaranteed to terminate with a correct model. We provide matching upper and lower bounds on the number of queries required by the algorithm, and report on the application of an implementation to some examples.

Although model checking is heavily used in the hardware domain, it did not take off in software engineering yet. One of the possible reasons is that software models are very complex. They integrate many dimensions such as data types and concurrency, leading to the infamous state space explosion problem. This article introduces the Algebraic Petri Nets Analyzer (AlPiNA), a symbolic model checker for High-level Petri nets. It is comprised of two independent modules: a GUI plug-in for Eclipse and an underlying model checking engine. AlPiNA is a step towards performing efficient and user-friendly model checking of large software systems. This is achieved by separating the model and its properties from the optimisation artifacts. This article describes the features that AlPiNA provides to the user for designing models and verifying properties. It also presents the techniques and artifacts used for tuning verification performance, along with some theoretical background.

The combined trace (i.e., comtrace) notion was introduced by Janicki and Koutny in 1995 as a generalization of the Mazurkiewicz trace notion. Comtraces are congruence classes of step sequences, where the congruence relation is defined from two relations simultaneity and serializability on events. They also showed that comtraces correspond to some class of labeled stratified order structures, but left open the question of what class of labeled stratified orders represents comtraces. In this work, we proposed a class of labeled stratified order structures that captures exactly the comtrace notion. Our main technical contributions are representation theorems showing that comtrace quotient monoid, combined dependency graph (Kleijn and Koutny 2008) and our labeled stratified order structure characterization are three different and yet equivalent ways to represent comtraces. This paper is a revised and expanded version of Lê (in Proceedings of PETRI NETS 2010, LNCS 6128, pp. 104-124).

Service-oriented computing proposes services as building blocks which can be composed to complex systems. To reason about the correctness of a service, its communication protocol needs to be analyzed. A fundamental correctness criterion for a service is the existence of a partner service, formalized in the notion of controllability. In this paper, we introduce Wendy, a Petri net-based tool to synthesize partner services. These partners are valuable artifacts to support the design, validation, verification, and adaptation of services. Furthermore, Wendy can calculate an operating guideline, a characterization of the set of all partners of a service. Operating guidelines can be used in many application scenarios from service brokerage to test case generation. Case studies show that Wendy efficiently performs on industrial service models.

Pure names are identifiers with no relation between them, except equality and inequality. In previous works we have extended P/T nets with the capability of creating and managing pure names, obtaining ν-PNs and proved that they are strictly well structured (WSTS), so that coverability and boundedness are decidable. Here we use the framework recently developed by Finkel and Goubault-Larrecq for forward analysis for WSTS, in the case of ν-PNs, to compute the cover, that gives a good over approximation of the set of reachable markings. We prove that the least complete domain containing the set of markings is effectively representable. Moreover, we prove that in the completion we can compute least upper bounds of simple loops. Therefore, a forward Karp-Miller procedure that computes the cover is applicable. However, we prove that in general the cover is not computable, so that the procedure is non-terminating in general. As a corollary, we obtain the analogous result for Transfer Data nets and Data Nets. Finally, we show that a slight modification of the forward analysis yields decidability of a weak form of boundedness called width-boundedness, and identify a subclass of ν-PN that we call dw-bounded ν-PN, for which the cover is computable.

A central problem in the area of Process Mining is to obtain a formal model that represents selected behavior of a system. The theory of regions has been applied to address this problem, enabling the derivation of a Petri net whose language includes a set of traces. However, when dealing with real-life systems, the available tool support for performing such a task is unsatisfactory, due to the complex algorithms that are required. In this paper, the theory of regions is revisited to devise a novel technique that explores the space of regions by combining the elements of a region basis. Due to its light space requirements, the approach can represent an important step for bridging the gap between the theory of regions and its industrial application. Experimental results show that there is improvement in orders of magnitude in comparison with state-of-the-art tools for the same task.

Literature on the stubborn set and similar state space reduction methods presents numerous seemingly ad-hoc conditions for selecting the transitions that are investigated in the current state. There are good reasons to believe that the choice between them has a significant effect on reduction results, but not much has been published on this topic. This article presents theoretical results and examples that aim at shedding light on the issue. Because the topic is extensive, we only consider the detection of deadlocks. We distinguish between different places where choices can be made and investigate their effects. It is usually impractical to aim at choices that are “best” in some sense. However, one non-trivial practical optimality result is proven.

Analysis of behavioural consistency is an important aspect of software engineering. In process and service management, consistency verification of behavioural models has manifold applications. For instance, a business process model used as system specification and a corresponding workflow model used as implementation have to be consistent. Another example would be the analysis to what degree a process log of executed business operations is consistent with the corresponding normative process model. Typically, existing notions of behaviour equivalence, such as bisimulation and trace equivalence, are applied as consistency notions. Still, these notions are exponential in computation and yield a Boolean result. In many cases, however, a quantification of behavioural deviation is needed along with concepts to isolate the source of deviation. In this article, we propose causal behavioural profiles as the basis for a consistency notion. These profiles capture essential behavioural information, such as order, exclusiveness, and causality between pairs of activities of a process model. Consistency based on these profiles is weaker than trace equivalence, but can be computed efficiently for a broad class of models. In this article, we introduce techniques for the computation of causal behavioural profiles using structural decomposition techniques for sound free-choice workflow systems if unstructured net fragments are acyclic or can be traced back to S- or T-nets. We also elaborate on the findings of applying our technique to three industry model collections.