On the computation of the minimal coverability set of Petri nets
| Autor: | Frédéric Servais, Pierre-Alain Reynier |
|---|---|
| Přispěvatelé: | Laboratoire d'Informatique et Systèmes (LIS), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Modélisation et Vérification (MOVE), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Département d'Informatique [Bruxelles] (ULB), Faculté des Sciences [Bruxelles] (ULB), Université libre de Bruxelles (ULB)-Université libre de Bruxelles (ULB) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Theoretical computer science
Computer science Efficient algorithm Computation media_common.quotation_subject 0102 computer and information sciences 02 engineering and technology Decision problem Petri net Infinity 01 natural sciences Set (abstract data type) Task (computing) [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] 010201 computation theory & mathematics Reachability Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing [INFO]Computer Science [cs] Computer Science::Formal Languages and Automata Theory media_common |
| Zdroj: | Reachability Problems 13th International Conference, RP 2019, Brussels, Belgium, September 11–13, 2019, Proceedings 13th International Conference on Reachability Problems 13th International Conference on Reachability Problems, Sep 2019, Bruxelles, Belgium. ⟨10.1007/978-3-030-30806-3_13⟩ Lecture Notes in Computer Science ISBN: 9783030308056 RP |
| DOI: | 10.1007/978-3-030-30806-3_13⟩ |
| Popis: | International audience; The verification of infinite-state systems is a challenging task. A prominent instance is reachability analysis of Petri nets, for which no efficient algorithm is known. The minimal coverability set of a Petri net can be understood as an approximation of its reachability set described by means of ω -markings (i.e. markings in which some entries may be set to infinity). It allows to solve numerous decision problems on Petri nets, such as any coverability problem. In this paper, we study the computation of the minimal coverability set.This set can be computed using the Karp and Miller trees, which perform accelerations of cycles along branches [10]. The resulting algorithm may however perform redundant computations. In a previous work [17], we proposed an improved algorithm allowing pruning between branches of the Karp and Miller tree, and proved its correctness. The proof of its correctness was complicated, as the introduction of pruning between branches may yield to incompleteness issues [5, 9].In this paper, we propose a new proof of the correctness of our algorithm. This new proof relies on an original invariant of the algorithm, leading to the following assets:1. it is considerably shorter and simpler,2. it allows to prove the correctness of a more generic algorithm, as the acceleration used is let as a parameter. Indeed, we identify the property that the acceleration should satisfy to ensure completeness.3. it opens the way to a generalization of our algorithm to extensions of Petri nets. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|