Fundamenta Informaticae - Volume 183, issue 3-4

Authors: Janicki, Ryszard | Lasota, Slawomir | Sidorova, Natalia

Article Type: Other

DOI: 10.3233/FI-2021-2085

Citation: Fundamenta Informaticae, vol. 183, no. 3-4, pp. i-ii, 2021

Authors: Allamigeon, Xavier | Boyet, Marin | Gaubert, Stéphane

Article Type: Research Article

Abstract: We study timed Petri nets, with preselection and priority routing. We represent the behavior of these systems by piecewise affine dynamical systems. We use tools from the theory of nonexpansive mappings to analyze these systems. We establish an equivalence theorem between priority-free fluid timed Petri nets and semi-Markov decision processes, from which we derive the convergence to a periodic regime and the polynomial-time computability of the throughput. More generally, we develop an approach inspired by tropical geometry, characterizing the congestion phases as the cells of a polyhedral complex. We illustrate these results by a current application to the performance evaluation …of emergency call centers in the Paris area. We show that priorities can lead to a paradoxical behavior: in certain regimes, the throughput of the most prioritary task may not be an increasing function of the resources. Show more

Keywords: Timed Petri net, Performance evaluation, Markov decision process, Tropical geometry, Emergency call center

DOI: 10.3233/FI-2021-2086

Citation: Fundamenta Informaticae, vol. 183, no. 3-4, pp. 169-201, 2021

Authors: Fahland, Dirk | Denisov, Vadim | van der Aalst, Wil. M.P.

Article Type: Research Article

Abstract: To identify the causes of performance problems or to predict process behavior, it is essential to have correct and complete event data. This is particularly important for distributed systems with shared resources, e.g., one case can block another case competing for the same machine, leading to inter-case dependencies in performance. However, due to a variety of reasons, real-life systems often record only a subset of all events taking place. To understand and analyze the behavior and performance of processes with shared resources, we aim to reconstruct bounds for timestamps of events in a case that must have happened but were …not recorded by inference over events in other cases in the system. We formulate and solve the problem by systematically introducing multi-entity concepts in event logs and process models. We introduce a partial-order based model of a multi-entity event log and a corresponding compositional model for multi-entity processes. We define PQR-systems as a special class of multi-entity processes with shared resources and queues. We then study the problem of inferring from an incomplete event log unobserved events and their timestamps that are globally consistent with a PQR-system. We solve the problem by reconstructing unobserved traces of resources and queues according to the PQR-model and derive bounds for their timestamps using a linear program. While the problem is illustrated for material handling systems like baggage handling systems in airports, the approach can be applied to other settings where recording is incomplete. The ideas have been implemented in ProM and were evaluated using both synthetic and real-life event logs. Show more

Keywords: Log repair, Process mining, Performance analysis, Multi-entity modeling, Multi-entity event logs, Conformance checking, Material handling systems

DOI: 10.3233/FI-2021-2087

Citation: Fundamenta Informaticae, vol. 183, no. 3-4, pp. 203-242, 2021

Authors: Finkel, Olivier | Skrzypczak, Michał

Article Type: Research Article

Abstract: We prove that ω -languages of (non-deterministic) Petri nets and ω -languages of (nondeterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of ω -languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of ω -languages of (non-deterministic) Turing machines. We also show that it is highly undecidable to determine the topological complexity of a Petri net ω -language. Moreover, we infer from the proofs of the above results that the equivalence and the inclusion problems for ω -languages of Petri nets are ∏ 2 1 …-complete, hence also highly undecidable. Additionally, we show that the situation is quite the opposite when considering unambiguous Petri nets, which have the semantic property that at most one accepting run exists on every input. We provide a procedure of determinising them into deterministic Muller counter machines with counter copying. As a consequence, we entail that the ω -languages recognisable by unambiguous Petri nets are △ 3 0 sets. Show more

Keywords: Automata and formal languages, Petri nets, Infinite words, Logic in computer science, Cantor topology, Borel hierarchy, Wadge degrees, Highly undecidable properties, Unambiguous Petri nets

DOI: 10.3233/FI-2021-2088

Citation: Fundamenta Informaticae, vol. 183, no. 3-4, pp. 243-291, 2021

Authors: Kalenkova, Anna | Carmona, Josep | Polyvyanyy, Artem | La Rosa, Marcello

Article Type: Research Article

Abstract: State-of-the-art process discovery methods construct free-choice process models from event logs. Consequently, the constructed models do not take into account indirect dependencies between events. Whenever the input behaviour is not free-choice, these methods fail to provide a precise model. In this paper, we propose a novel approach for enhancing free-choice process models by adding non-free-choice constructs discovered a-posteriori via region-based techniques. This allows us to benefit from the performance of existing process discovery methods and the accuracy of the employed fundamental synthesis techniques. We prove that the proposed approach preserves fitness with respect to the event log while improving the …precision when indirect dependencies exist. The approach has been implemented and tested on both synthetic and real-life datasets. The results show its effectiveness in repairing models discovered from event logs. Show more

Keywords: free-choice Petri nets, region state-based synthesis, event logs, transition systems, process mining, process enhancement

DOI: 10.3233/FI-2021-2089

Citation: Fundamenta Informaticae, vol. 183, no. 3-4, pp. 293-317, 2021

Authors: Thierry-Mieg, Yann

Article Type: Research Article

Abstract: Brute-force model-checking consists in exhaustive exploration of the state-space of a Petri net, and meets the dreaded state-space explosion problem. In contrast, this paper shows how to solve model-checking problems using a combination of techniques that stay in complexity proportional to the size of the net structure rather than to the state-space size. We combine an SMT based over-approximation to prove that some behaviors are unfeasible, an under-approximation using memory-less sampling of runs to find witness traces or counter-examples, and a set of structural reduction rules that can simplify both the system and the property. This approach …was able to win by a clear margin the model-checking contest 2020 for reachability queries as well as deadlock detection, thus demonstrating the practical effectiveness and general applicability of the system of rules presented in this paper. Show more

Keywords: Petri nets, Structural Reduction, Model-checking, SMT constraints

DOI: 10.3233/FI-2021-2090

Citation: Fundamenta Informaticae, vol. 183, no. 3-4, pp. 319-342, 2021