Avoid One's Doom: Finding Cliff-Edge Configurations in Petri Nets
| Autor: | Aguirre-Samboní, Giann Karlo, Haar, Stefan, Paulevé, Loïc, Schwoon, Stefan, Würdemann, Nick |
|---|---|
| Přispěvatelé: | Modeling and Exploitation of Interaction and Concurrency (MEXICO), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Centre National de la Recherche Scientifique (CNRS), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Fachbereich Informatik - Oldenburg, Carl Von Ossietzky Universität Oldenburg = Carl von Ossietzky University of Oldenburg (OFFIS), DIGICOSME grant ESCAPE , DIGICOSME RD 242-ESCAPE-15203, ANR-20-CE45-0001,BNeDiction,Ensembles de Réseaux Booléens Prédictifs(2020) |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: |
FOS: Computer and information sciences
[INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] Formal Languages and Automata Theory (cs.FL) Computer Science - Data Structures and Algorithms [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH] Computer Science - Formal Languages and Automata Theory Data Structures and Algorithms (cs.DS) ACM: F.: Theory of Computation ACM: G.: Mathematics of Computing |
| Zdroj: | GandALF 2022-Games, Automata, Logics, and Formal Verification GandALF 2022-Games, Automata, Logics, and Formal Verification, Sep 2022, Madrid, Spain. ⟨10.4204/EPTCS.370.12⟩ |
| DOI: | 10.4204/EPTCS.370.12⟩ |
| Popis: | A crucial question in analyzing a concurrent system is to determine its long-run behaviour, and in particular, whether there are irreversible choices in its evolution, leading into parts of the reachability space from which there is no return to other parts. Casting this problem in the unifying framework of safe Petri nets, our previous work has provided techniques for identifying attractors, i.e. terminal strongly connected components of the reachability space, whose attraction basins we wish to determine. Here, we provide a solution for the case of safe Petri nets. Our algorithm uses net unfoldings and provides a map of all of the system's configurations (concurrent executions) that act as cliff-edges, i.e. any maximal extension for those configurations lies in some basin that is considered fatal. The computation turns out to require only a relatively small prefix of the unfolding, just twice the depth of Esparza's complete prefix. Comment: In Proceedings GandALF 2022, arXiv:2209.09333. This work was supported by the DIGICOSME grant ESCAPE DIGICOSME RD 242-ESCAPE-15203 and by the French Agence Nationale pour la Recherche (ANR) in the scope of the project ''BNeDiction'' (grant number ANR-20-CE45-0001) |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|