Ideal Decompositions for Vector Addition Systems

Jérôme Leroux 1 Sylvain Schmitz 2, 3
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : Vector addition systems, or equivalently Petri nets, are one of the most popular formal models for the representation and the analysis of parallel processes. Many problems for vector addition systems are known to be decidable thanks to the theory of well-structured transition systems. Indeed, vector addition systems with configurations equipped with the classical point-wise ordering are well-structured transition systems. Based on this observation, problems like coverability or termination can be proven decidable. However, the theory of well-structured transition systems does not explain the decidability of the reachability problem. In this presentation, we show that runs of vector addition systems can also be equipped with a well quasi-order. This observation provides a unified understanding of the data structures involved in solving many problems for vector addition systems, including the central reachability problem.
Type de document :
Communication dans un congrès
Nicolas Ollinger and Heribert Vollmer. STACS 2016 - 33rd Symposium on Theoretical Aspects of Computer Science, 2016, Orléans, France. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 47, pp.1--13, 2016, Leibniz International Proceedings in Informatics (LIPIcs). 〈http://drops.dagstuhl.de/opus/volltexte/2016/5702〉. 〈10.4230/LIPIcs.STACS.2016.1〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01275991
Contributeur : Sylvain Schmitz <>
Soumis le : jeudi 18 février 2016 - 15:55:28
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14

Identifiants

Citation

Jérôme Leroux, Sylvain Schmitz. Ideal Decompositions for Vector Addition Systems. Nicolas Ollinger and Heribert Vollmer. STACS 2016 - 33rd Symposium on Theoretical Aspects of Computer Science, 2016, Orléans, France. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 47, pp.1--13, 2016, Leibniz International Proceedings in Informatics (LIPIcs). 〈http://drops.dagstuhl.de/opus/volltexte/2016/5702〉. 〈10.4230/LIPIcs.STACS.2016.1〉. 〈hal-01275991〉

Partager

Métriques

Consultations de la notice

357