Fundamenta Informaticae - Volume 187, issue 2-4

Authors: Buchs, Didier | Carmona, Josep | Kleijn, Jetty

Article Type: Other

DOI: 10.3233/FI-222132

Citation: Fundamenta Informaticae, vol. 187, no. 2-4, pp. i-iii, 2022

Authors: Abbes, Samy

Article Type: Research Article

Abstract: The first part of the paper is an introduction to the theory of probabilistic concurrent systems under a partial order semantics. Key definitions and results are given and illustrated on examples. The second part includes contributions. We introduce deterministic concurrent systems as a subclass of concurrent systems. Deterministic concurrent system are “locally commutative” concurrent systems. We prove that irreducible and deterministic concurrent systems have a unique probabilistic dynamics, and we characterize these systems by means of their combinatorial properties. ACM CSS: G.2.1; F.1.1

DOI: 10.3233/FI-222133

Citation: Fundamenta Informaticae, vol. 187, no. 2-4, pp. 71-102, 2022

Authors: Amat, Nicolas | Berthomieu, Bernard | Dal Zilio, Silvano

Article Type: Research Article

Abstract: We define a new method for taking advantage of net reductions in combination with a SMT-based model checker. Our approach consists in transforming a reachability problem about some Petri net, into the verification of an updated reachability property on a reduced version of this net. This method relies on a new state space abstraction based on systems of constraints, called polyhedral abstraction. We prove the correctness of this method using a new notion of equivalence between nets. We provide a complete framework to define and check the correctness of equivalence judgements; prove that this relation is a congruence; and …give examples of basic equivalence relations that derive from structural reductions. Our approach has been implemented in a tool, named SMPT, that provides two main procedures: Bounded Model Checking (BMC) and Property Directed Reachability (PDR). Each procedure has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries used in the Model Checking Contest. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions. Show more

DOI: 10.3233/FI-222134

Citation: Fundamenta Informaticae, vol. 187, no. 2-4, pp. 103-138, 2022

Authors: Devillers, Raymond | Tredup, Ronny

Article Type: Research Article

Abstract: Petri net synthesis consists in deciding for a given transition system A whether there exists a Petri net N whose reachability graph is isomorphic to A . Several works examined the synthesis of Petri net subclasses that restrict, for every place p of the net, the cardinality of its preset or of its postset or both in advance by small natural numbers ϱ and κ , respectively, such as for example (weighted) marked graphs, (weighted) T-systems and choice-free nets. In this paper, we study the synthesis aiming at Petri nets which have such restricted …place environments, from the viewpoint of classical and parameterized complexity: We first show that, for any fixed natural numbers ϱ and κ , deciding whether for a given transition system A there is a Petri net N such that (1) its reachability graph is isomorphic to A and (2) for every place p of N the preset of p has at most ϱ and the postset of p has at most κ elements is doable in polynomial time. Secondly, we introduce a modified version of the problem, namely ENVIRONMENT RESTRICTED SYNTHESIS (ERS, for short), where ϱ and κ are part of the input, and show that ERS is NPcomplete, regardless whether the sought net is impure or pure. In case of the impure nets, our methods also imply that ERS parameterized by ϱ + κ is W [2]-hard. Show more

DOI: 10.3233/FI-222135

Citation: Fundamenta Informaticae, vol. 187, no. 2-4, pp. 139-165, 2022

Authors: Devillers, Raymond | Tredup, Ronny

Article Type: Research Article

Abstract: In Petri net synthesis we ask whether a given transition system A can be implemented by a Petri net N . Depending on the level of accuracy, there are three ways how N can implement A : an embedding , the least accurate implementation, preserves only the diversity of states of A ; a language simulation already preserves exactly the language of A ; a realization , the most accurate implementation, realizes the behavior of A exactly. However, whatever the sought implementation, a corresponding net does not always exist. In this case, it was suggested to …modify the input behavior – of course as little as possible. Since transition systems consist of states, events and edges, these components appear as a natural choice for modifications. In this paper we show that the task of converting an unimplementable transition system into an implementable one by removing as few states or events or edges as possible is NP-complete –regardless of what type of implementation we are aiming for; we also show that the corresponding parameterized problems are W [2]-hard, where the number of removed components is considered as the parameter; finally, we show there is no c -approximation algorithm (with a polynomial running time) for neither of these problems, for every constant c ≥ 1. Show more

DOI: 10.3233/FI-222136

Citation: Fundamenta Informaticae, vol. 187, no. 2-4, pp. 167-196, 2022

Authors: Esparza, Javier | Raskin, Mikhail | Welzel, Christoph

Article Type: Research Article

Abstract: A fundamental advantage of Petri net models is the possibility to automatically compute useful system invariants from the syntax of the net. Classical techniques used for this are place invariants, P-components, siphons or traps. Recently, Bozga et al. have presented a novel technique for the parameterized verification of safety properties of systems with a ring or array architecture. They show that the statement “for every instance of the parameterized Petri net, all markings satisfying the linear invariants associated to all the P-components, siphons and traps of the instance are safe” can be encoded in WS1S and checked using tools …like MONA. However, while the technique certifies that this infinite set of linear invariants extracted from P-components, siphons or traps are strong enough to prove safety, it does not return an explanation of this fact understandable by humans. We present a CEGAR loop that constructs a finite set of parameterized P-components, siphons or traps, whose infinitely many instances are strong enough to prove safety. For this we design parameterization procedures for different architectures. Show more

Keywords: parameterized systems, logic, theorem proving, first-order, WS1S

DOI: 10.3233/FI-222137

Citation: Fundamenta Informaticae, vol. 187, no. 2-4, pp. 197-243, 2022

Authors: Wallner, Sophie | Wolf, Karsten

Article Type: Research Article

Abstract: Uniform coloured Petri nets can be abstracted to their skeleton , the place/transition net that simply turns the coloured tokens into black tokens. A coloured net and its skeleton are related by a net morphism [1, 2]. For the application of the skeleton as an abstraction method in the model checking process, we need to establish a simulation relation [3] between the state spaces of the two nets. Then, universal temporal properties (properties of the ACTL * logic) are preserved. The abstraction relation induced by a net morphism is not necessarily a simulation relation, due to a subtle …issue related to deadlocks [4]. We discuss several situations where the abstraction relation induced by a net morphism is as well a simulation relation, thus preserving ACTL * properties. We further propose a partition refinement algorithm for folding a place/transition net into a coloured net. This way, skeleton abstraction becomes available for models given as place/transition nets. Experiments demonstrate the capabilities of the proposed technology. Using skeleton abstraction, we are capable of solving problems that have not been solved before in the Model Checking Contest [5]. Show more

DOI: 10.3233/FI-222138

Citation: Fundamenta Informaticae, vol. 187, no. 2-4, pp. 245-272, 2022