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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-01275991
Contributor : Sylvain Schmitz <>
Submitted on : Thursday, February 18, 2016 - 3:55:28 PM
Last modification on : Tuesday, February 5, 2019 - 1:46:02 PM

Identifiers

Citation

Jérôme Leroux, Sylvain Schmitz. Ideal Decompositions for Vector Addition Systems. STACS 2016 - 33rd Symposium on Theoretical Aspects of Computer Science, 2016, Orléans, France. pp.1--13, ⟨10.4230/LIPIcs.STACS.2016.1⟩. ⟨hal-01275991⟩

Share

Metrics

Record views

457