Fundamenta Informaticae - Volume 131, issue 1

Authors: Haddad, Serge | Kleijn, Jetty | Pomello, Lucia

Article Type: Other

DOI: 10.3233/FI-2014-1001

Citation: Fundamenta Informaticae, vol. 131, no. 1, pp. v-vi, 2014

Authors: Valmari, Antti | Hansen, Henri

Article Type: Research Article

Abstract: Many algorithms for computing minimal coverability sets for Petri nets prune futures. That is, if a newmarking strictly covers an old one, then not just the old marking but also some subset of its successor markings is discarded from search. In this publication, a simpler algorithm that lacks future pruning is presented and proven correct. Its performance is compared with future pruning. It is demonstrated, using examples, that neither approach is systematically better than the other. However, the simple algorithm has some attractive features. It never needs to re-construct pruned parts of the minimal coverability set. It automatically gives most …of the advantage of future pruning, if the minimal coverability set is constructed in depth-first or most tokens first order, and if so-called history merging is applied. Some implementation aspects of minimal coverability set construction are also discussed. Some measurements are given to demonstrate the effect of construction order and other implementation aspects. Show more

DOI: 10.3233/FI-2014-1002

Citation: Fundamenta Informaticae, vol. 131, no. 1, pp. 1-25, 2014

Authors: Evangelista, Sami | Kristensen, Lars Michael

Article Type: Research Article

Abstract: The sweep-line method allows explicit state model checkers to delete states from memory on-the-fly during state space exploration, thereby lowering the memory demands of the verification procedure. The sweep-line method is based on a least-progress-first search order that prohibits the immediate use of standard on-the-fly Büchi automata-based model checking algorithms that rely on a depth-first search order in the search for an acceptance cycle. This paper proposes and experimentally evaluates an algorithm for Büchi automata-based model checking compatible with the search order and deletion of states prescribed by the sweep-line method.

DOI: 10.3233/FI-2014-1003

Citation: Fundamenta Informaticae, vol. 131, no. 1, pp. 27-53, 2014

Authors: Martos-Salgado, María | Rosa-Velardo, Fernando

Article Type: Research Article

Abstract: We extend workflow Petri nets (wf-nets) with discrete prices, by associating a price to the execution of a transition and to the storage of tokens. We first define the safety and the soundness problems for priced wf-nets. A priced wf-net is safe if no execution costs more than a given budget. The soundness problem is that of deciding whether the workflow can always terminate properly, where in the priced setting “properly” also means that the execution does not cost more than a given threshold. Then, we study safety and soundness of resource-constrained workflow nets (rcwf-nets), an extension of wf-nets for …the modeling of concurrent executions of a workflow, sharing some global resources. We develop a framework in which to study safety and soundness for priced rcwf-nets, that is parametric on the cost model. Then, that framework is instantiated, obtaining the cases in which the sum, the maximum, the average and the discounted sum of the prices of all instances are considered. We study the decidability and the complexity of these properties, together with their relation. Show more

DOI: 10.3233/FI-2014-1004

Citation: Fundamenta Informaticae, vol. 131, no. 1, pp. 55-80, 2014

Authors: Liu, GuanJun | Sun, Jun | Liu, Yang | Dong, JinSong

Article Type: Research Article

Abstract: Classical workflow nets (WF-nets for short) are an important subclass of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property of workflow systems and guarantees that these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable for WF-nets and can be polynomially solvable for free-choice WF-nets. This paper proves that the soundness problem is PSPACE-hard for WF-nets. Furthermore, it is proven that the soundness problem is PSPACE-complete for bounded WF-nets. Based on the above conclusion, it is derived that the soundness problem is also PSPACE-complete for …bounded WF-nets with reset or inhibitor arcs (ReWF-nets and InWF-nets for short, resp.). ReWF- and InWF-nets are two extensions to WF-nets and their soundness problems were proven by Aalst et al. to be undecidable. Additionally, we prove that the soundness problem is co-NP-hard for asymmetric-choice WF-nets that are a larger class and can model more cases of interaction and resource allocation than free-choice ones. Show more

Keywords: Workflow Nets, Soundness, Complexity, PSPACE-hardness, co-NP-hardness

DOI: 10.3233/FI-2014-1005

Citation: Fundamenta Informaticae, vol. 131, no. 1, pp. 81-101, 2014

Authors: van der Aalst, W.M.P. | Verbeek, H.M.W.

Article Type: Research Article

Abstract: The two most prominent process mining tasks are process discovery (i.e., learning a process model from an event log) and conformance checking (i.e., diagnosing and quantifying differences between observed and modeled behavior). The increasing availability of event data makes these tasks highly relevant for process analysis and improvement. Therefore, process mining is considered to be one of the key technologies for Business Process Management (BPM). However, as event logs and process models grow, process mining becomes more challenging. Therefore, we propose an approach to decompose process mining problems into smaller problems using the notion of passages. A passage is a …pair of two non-empty sets of activities (X, Y) such that the set of direct successors of X is Y and the set of direct predecessors of Y is X. Any Petri net can be partitioned using passages. Moreover, process discovery and conformance checking can be done per passage and the results can be aggregated. This has advantages in terms of efficiency and diagnostics. Moreover, passages can be used to distribute process mining problems over a network of computers. Passages are supported through ProM plug-ins that automatically decompose process discovery and conformance checking tasks. Show more

Keywords: process mining, conformance checking, process discovery, distributed computing, business process management

DOI: 10.3233/FI-2014-1006

Citation: Fundamenta Informaticae, vol. 131, no. 1, pp. 103-138, 2014

Authors: Gil-Costa, Veronica | Marin, Mauricio | Inostrosa-Psijas, Alonso | Lobos, Jair | Bonacic, Carolina

Article Type: Research Article

Abstract: This paper proposes using Coloured Petri Nets to model performance of vertical search engines for Web search. In such systems, queries submitted by users or client systems are handled by different components implemented as services deployed on large clusters of dedicated processors. We propose models that represent key features of components running time cost at a suitable level of detail. A comprehensive evaluation study is presented to reveal good precision of models when compared against actual implementations and complex process-oriented simulators of the same search engine instances. A C++ class library is proposed to enable rapid model construction by using …a hierarchical and scalable approach, and to enable transparent generation and efficient execution of respective simulation programs either sequentially or in parallel. Show more

Keywords: Web search engines, Petri net applications, performance evaluation and modelling

DOI: 10.3233/FI-2014-1007

Citation: Fundamenta Informaticae, vol. 131, no. 1, pp. 139-166, 2014