Document Open Access Logo

Flattability of Priority Vector Addition Systems

Author Roland Guttenberg

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.141.pdf
  • Filesize: 0.81 MB
  • 20 pages

Document Identifiers

Author Details

Roland Guttenberg
  • Technical University of Munich, Germany

Acknowledgements

I thank my PhD advisor Javier Esparza for reading a first draft and providing feedback. I thank the anonymous reviewers for their helpful feedback.

Cite AsGet BibTex

Roland Guttenberg. Flattability of Priority Vector Addition Systems. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 141:1-141:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.141

Abstract

Vector addition systems (VAS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VAS, which consists of deciding whether a target configuration of a VAS is reachable from a given initial configuration. One of the main approaches to solve the problem on practical instances is called flattening, intuitively removing nested loops. This technique is known to terminate for semilinear VAS due to [Jérôme Leroux, 2013]. In this paper, we prove that also for VAS with nested zero tests, called Priority VAS, flattening does in fact terminate for all semilinear reachability relations. Furthermore, we prove that Priority VAS admit semilinear inductive invariants. Both of these results are obtained by defining a well-quasi-order on runs of Priority VAS which has good pumping properties.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Priority Vector Addition Systems
  • Semilinear
  • Inductive Invariants
  • Geometry
  • Flattability
  • Almost Semilinear
  • Transformer Relation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Mohamed Faouzi Atig and Pierre Ganty. Approximating petri net reachability along context-free traces. In FSTTCS, volume 13 of LIPIcs, pages 152-163. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. Google Scholar
  2. Michael Blondin and François Ladouceur. Population protocols with unordered data. In ICALP, volume 261 of LIPIcs, pages 115:1-115:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  3. Rémi Bonnet. The reachability problem for vector addition system with one zero-test. In MFCS, volume 6907 of Lecture Notes in Computer Science, pages 145-157. Springer, 2011. Google Scholar
  4. Rémi Bonnet. Theory of Well-Structured Transition Systems and Extended Vector-Addition Systems. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, 2013. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bonnet-phd13.pdf.
  5. Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Separability of reachability sets of vector addition systems. In STACS, volume 66 of LIPIcs, pages 24:1-24:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  6. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for petri nets is not elementary. In STOC, pages 24-33. ACM, 2019. Google Scholar
  7. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In FOCS, pages 1229-1240. IEEE, 2021. Google Scholar
  8. Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for two-counter machines with one test and one reset. In FSTTCS, volume 122 of LIPIcs, pages 31:1-31:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  9. Roland Guttenberg. Flattability of priority vector addition systems, 2024. URL: https://arxiv.org/abs/2402.09185.
  10. Roland Guttenberg, Mikhail A. Raskin, and Javier Esparza. Geometry of reachability sets of vector addition systems. In CONCUR, volume 279 of LIPIcs, pages 6:1-6:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  11. Christoph Haase. A survival guide to presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. Google Scholar
  12. Christoph Haase and Georg Zetzsche. Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. In LICS, pages 1-14. IEEE, 2019. Google Scholar
  13. Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Sylvain Schmitz, and Patrick Totzke. Coverability trees for petri nets with unordered data. In FoSSaCS, volume 9634 of Lecture Notes in Computer Science, pages 445-461. Springer, 2016. Google Scholar
  14. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135-159, 1979. Google Scholar
  15. Petr Jancar. Decidability of a temporal logic problem for petri nets. Theor. Comput. Sci., 74(1):71-93, 1990. Google Scholar
  16. S. Rao Kosaraju. Decidability of reachability in vector addition systems. In STOC, pages 267-281. ACM, 1982. Google Scholar
  17. Jean-Luc Lambert. A structure to decide reachability in petri nets. Theor. Comput. Sci., 99(1):79-104, 1992. Google Scholar
  18. Ranko Lazic and Sylvain Schmitz. The complexity of coverability in ν-petri nets. In LICS, pages 467-476. ACM, 2016. Google Scholar
  19. Jérôme Leroux. The general vector addition system reachability problem by presburger inductive invariants. In LICS, pages 4-13. IEEE Computer Society, 2009. Google Scholar
  20. Jérôme Leroux. Vector addition system reachability problem: A short self-contained proof. In LATA, volume 6638 of Lecture Notes in Computer Science, pages 41-64. Springer, 2011. Google Scholar
  21. Jérôme Leroux. Vector addition systems reachability problem (A simpler solution). In Turing-100, volume 10 of EPiC Series in Computing, pages 214-228. EasyChair, 2012. Google Scholar
  22. Jérôme Leroux. Presburger vector addition systems. In LICS, pages 23-32. IEEE Computer Society, 2013. URL: https://hal.science/hal-00780462v2.
  23. Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. In FOCS, pages 1241-1252. IEEE, 2021. Google Scholar
  24. Jérôme Leroux, M. Praveen, Philippe Schnoebelen, and Grégoire Sutre. On functions weakly computable by pushdown petri nets and related systems. Log. Methods Comput. Sci., 15(4), 2019. Google Scholar
  25. Jérôme Leroux, M. Praveen, and Grégoire Sutre. Hyper-ackermannian bounds for pushdown vector addition systems. In CSL-LICS, pages 63:1-63:10. ACM, 2014. Google Scholar
  26. Jérôme Leroux and Grégoire Sutre. Reachability in two-dimensional vector addition systems with states: One test is for free. In CONCUR, volume 171 of LIPIcs, pages 37:1-37:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  27. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In ICALP (2), volume 9135 of Lecture Notes in Computer Science, pages 324-336. Springer, 2015. Google Scholar
  28. Ernst W. Mayr. An algorithm for the general petri net reachability problem. In STOC, pages 238-246. ACM, 1981. Google Scholar
  29. Ruzica Piskac and Viktor Kuncak. Linear arithmetic with stars. In CAV, volume 5123 of Lecture Notes in Computer Science, pages 268-280. Springer, 2008. Google Scholar
  30. Klaus Reinhardt. Reachability in petri nets with inhibitor arcs. In RP, volume 223 of Electronic Notes in Theoretical Computer Science, pages 239-264. Elsevier, 2008. Google Scholar
  31. Fernando Rosa-Velardo and David de Frutos-Escrig. Decidability and complexity of petri nets with unordered data. Theor. Comput. Sci., 412(34):4439-4451, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact