Fundamenta Informaticae - Volume 169, issue 1-2

Authors: Khomenko, Victor | Kleijn, Jetty | Penczek, Wojciech | Roux, Olivier H.

Article Type: Other

DOI: 10.3233/FI-2019-1836

Citation: Fundamenta Informaticae, vol. 169, no. 1-2, pp. v-vi, 2019

Authors: Devillers, Raymond | Hujsa, Thomas

Article Type: Research Article

Abstract: Numerous real-world systems can be modeled with Petri nets, which allow a combination of concurrency with synchronizations and conflicts. To alleviate the difficulty of checking their behaviour, a common approach consists in studying specific subclasses. In the converse problem of Petri net synthesis, a Petri net of some subclass has to be constructed efficiently from a given specification, typically from a labelled transition system (lts) describing the behaviour of the desired net. In this paper, we focus on a notorious subclass of persistent Petri nets, the weighted marked graphs (WMGs), also called generalised (or weighted) event (or marked) graphs …or weighted T-nets. In such nets, edges have multiplicities (weights) and each place has at most one ingoing and one outgoing transition. Although extensively studied in previous works and benefiting from strong results, both their analysis and synthesis can be further investigated. We provide new behavioural properties of WMGs expressed on their reachability graph, notably backward persistence and strong similarities between any two sequences sharing the same starting state and the same destination state. Besides, we design a general synthesis procedure aiming at the WMG class. Finally, when no solution to the synthesis problem exists, i.e., when the given lts is not WMG-solvable, we show how to construct a WMG whose reachability graph is a minimal over-approximation of the given lts. Show more

Keywords: Weighted Petri net, analysis, synthesis, marked graph, event graph, theory of regions, approximation, persistence

DOI: 10.3233/FI-2019-1837

Citation: Fundamenta Informaticae, vol. 169, no. 1-2, pp. 1-30, 2019

Authors: Janicki, Ryszard | Koutny, Maciej

Article Type: Research Article

Abstract: A representation of interval orders by sequences of antichains is discussed, and its relationship to the Fishburn’s representation by sequences of the beginnings and endings of domain elements is analysed in detail. Moreover, an operational semantics based on sequences of maximal antichains is proposed and investigated for a general class of safe Petri nets with context arcs.

Keywords: interval order, operational semantics, Petri net, sequence of maximal antichains, interval sequence

DOI: 10.3233/FI-2019-1838

Citation: Fundamenta Informaticae, vol. 169, no. 1-2, pp. 31-55, 2019

Authors: Wolf, Karsten

Article Type: Research Article

Abstract: We propose a new algorithmic approach for the synthesis of a Petri net from a transition system. It is first presented for a class of place/transition Petri nets we call Δ1-Petri nets. A Δ1-Petri net has an incidence matrix where entries have values 0, 1, and -1 only. The algorithm employs Tarjans union/find algorithm for managing sets of vertices. It requires just O (|V ||T |) space where V is the set of vertices and T is the set of transition labels. Consequently, problem instances even beyond 1,000,000 vertices have a manageable memory footprint. Our results are experimentally …validated using a prototype implementation. We further present ideas for adapting the method to various classes of Petri nets, including pure (loop-free), safe and k -bounded, ordinary nets as subclasses of Δ-1-Petri nets as well as an extension to Δk -Petri nets. This article is an extended version of [1]. Show more

DOI: 10.3233/FI-2019-1839

Citation: Fundamenta Informaticae, vol. 169, no. 1-2, pp. 57-84, 2019

Authors: Valk, Rüdiger

Article Type: Research Article

Abstract: Cycloids are particular Petri nets for modelling processes of actions or events. They belong to the fundaments of Petri’s general systems theory and have very different interpretations, ranging from Einstein’s relativity theory to elementary information processing gates. Despite their simple definitions, their properties are still not completely understood. This contribution provides for the first time a formal definition together with new results concerning their structure. Cycloids are proved to be live and safe. It is shown that the minimal length of a cycle is the length of a local basic circuit, possibly decreased by an integer multiple of the number …of semi-active transitions. These results allow to find the defining parameters of a cycloid from the static properties of the net system. Similar results are obtained for degenerate cycloids. Show more

Keywords: Analysis and Synthesis of Petri nets, Structure of Petri Nets, Cycloids, General Net Theory, Degenerate Cycloids

DOI: 10.3233/FI-2019-1840

Citation: Fundamenta Informaticae, vol. 169, no. 1-2, pp. 85-121, 2019

Authors: Jančar, Petr | Leroux, Jérôme | Sutre, Grégoire

Article Type: Research Article

Abstract: The boundedness problem is a well-known exponential-space complete problem for vector addition systems with states (or Petri nets); it asks if the reachability set (for a given initial configuration) is finite. Here we consider a dual problem, the co-finiteness problem that asks if the complement of the reachability set is finite; by restricting the question we get the co-emptiness (or universality) problem that asks if all configurations are reachable. We show that both the co-finiteness problem and the co-emptiness problem are exponential-space complete. While the lower bounds are obtained by a straightforward reduction from coverability, getting the upper bounds …is more involved; in particular we use the bounds derived for reversible reachability by Leroux (2013). The studied problems were motivated by a result for structural liveness of Petri nets; this problem was shown decidable by Jančar (2017), without clarifying its complexity. The structural liveness problem is tightly related to a generalization of the co-emptiness problem, where the sets of initial configurations are (possibly infinite) downward closed sets instead of just singletons. We formulate the problems even more generally, for semilinear sets of initial configurations; in this case we show that the co-emptiness problem is decidable (without giving an upper complexity bound), and we formulate a conjecture under which the co-finiteness problem is also decidable. Show more

Keywords: vector addition system, Petri net, co-finite reachability set, universal reachability set, structural liveness, complexity

DOI: 10.3233/FI-2019-1841

Citation: Fundamenta Informaticae, vol. 169, no. 1-2, pp. 123-150, 2019

Authors: van der Aalst, Wil M.P.

Article Type: Research Article

Abstract: A process model is lucent if no two reachable states are enabling the same set of activities. An event log is translucent if each event carries information about the set of activities enabled when the event occurred (normally one only sees the activity performed). Both lucency and translucency focus on the set of enabled activities and are therefore related. Surprisingly, these notions have not been investigated before. This paper aims to (1) characterize process models that are lucent, (2) provide a discovery approach to learn process models from translucent event logs, and (3) relate lucency and translucency. …Lucency is defined both in terms of automata and Petri nets. A marked Petri net is lucent if there are no two different reachable markings enabling the same set of transitions, i.e., states are fully characterized by the transitions they enable. We will also provide a novel process discovery technique starting from a translucent event log. It turns out that information about the set of activities is extremely valuable for process discovery. We will provide sufficient conditions to ensure that the discovered model is lucent and show that a translucent event log sampled from a lucent process model can be used to rediscover the original model. We anticipate new analysis techniques exploiting lucency. Moreover, as shown in this paper, translucent event logs provide valuable information that can be exploited by a new breed to process mining techniques. Show more

Keywords: Process mining, Petri nets, lucent process models, translucent event logs

DOI: 10.3233/FI-2019-1842

Citation: Fundamenta Informaticae, vol. 169, no. 1-2, pp. 151-177, 2019