Document Open Access Logo

Improved Algorithm for Reachability in d-VASS

Authors Yuxi Fu, Qizhe Yang , Yangluo Zheng

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.136.pdf
  • Filesize: 0.85 MB
  • 18 pages

Document Identifiers

Author Details

Yuxi Fu
  • BASICS, Shanghai Jiao Tong University, China
Qizhe Yang
  • Shanghai Normal University, China
Yangluo Zheng
  • BASICS, Shanghai Jiao Tong University, China

Funding

The support from the National Natural Science Foundation of China (62072299) is acknowledged.

Acknowledgements

We thank Weijun Chen, Huan Long, Hao Wu and Qiang Yin for proofreading various versions of this paper.

Cite AsGet BibTex

Yuxi Fu, Qizhe Yang, and Yangluo Zheng. Improved Algorithm for Reachability in d-VASS. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 136:1-136:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.136

Abstract

An 𝖥_{d} upper bound for the reachability problem in vector addition systems with states (VASS) in fixed dimension is given, where 𝖥_d is the d-th level of the Grzegorczyk hierarchy of complexity classes. The new algorithm combines the idea of the linear path scheme characterization of the reachability in the 2-dimension VASSes with the general decomposition algorithm by Mayr, Kosaraju and Lambert. The result improves the 𝖥_{d + 4} upper bound due to Leroux and Schmitz (LICS 2019).

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Logic and verification
Keywords
  • Petri net
  • vector addition system
  • reachability

Metrics

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

Related Versions

References

  1. Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazic, Pierre McKenzie, and Patrick Totzke. The reachability problem for two-dimensional vector addition systems with states. J. ACM, 68(5):34:1-34:43, 2021. URL: https://doi.org/10.1145/3464794.
  2. Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in two-dimensional vector addition systems with states is pspace-complete. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 32-43. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.14.
  3. Dmitry Chistikov and Christoph Haase. The taming of the semi-linear set. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 128:1-128:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.ICALP.2016.128.
  4. E. A. Cichon and Elias Tahhan-Bittar. Ordinal recursive bounds for higman’s theorem. Theor. Comput. Sci., 201(1-2):63-84, 1998. URL: https://doi.org/10.1016/S0304-3975(97)00009-1.
  5. Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, Jérôme Leroux, and Lukasz Orlikowski. New lower bounds for reachability in vector addition systems. In Patricia Bouyer and Srikanth Srinivasan, editors, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023, December 18-20, 2023, IIIT Hyderabad, Telangana, India, volume 284 of LIPIcs, pages 35:1-35:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2023.35.
  6. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  7. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer Science, pages 369-383. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_25.
  8. Peter Habermehl, Roland Meyer, and Harro Wimmel. The downward-closure of petri net languages. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 466-477. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14162-1_39.
  9. Thomas Jech. Set Theory. Springer Monographs in Mathematics. Springer, 2003. URL: https://doi.org/10.1007/3-540-44761-X.
  10. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC '82, pages 267-281, New York, NY, USA, 1982. Association for Computing Machinery. URL: https://doi.org/10.1145/800070.802201.
  11. Jean-Luc Lambert. A structure to decide reachability in petri nets. Theor. Comput. Sci., 99(1):79-104, 1992. URL: https://doi.org/10.1016/0304-3975(92)90173-D.
  12. Jérôme Leroux. Flat petri nets (invited talk). In Didier Buchs and Josep Carmona, editors, Application and Theory of Petri Nets and Concurrency - 42nd International Conference, PETRI NETS 2021, Virtual Event, June 23-25, 2021, Proceedings, volume 12734 of Lecture Notes in Computer Science, pages 17-30. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-76983-3_2.
  13. Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  14. Jérôme Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 56-67. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.16.
  15. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  16. Jérôme Leroux and Grégoire Sutre. On flatness for 2-dimensional vector addition systems with states. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_26.
  17. Ernst W. Mayr. An algorithm for the general petri net reachability problem. In Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computing, STOC '81, pages 238-246, New York, NY, USA, 1981. Association for Computing Machinery. URL: https://doi.org/10.1145/800076.802477.
  18. Loic Pottier. Minimal solutions of linear diophantine systems: Bounds and algorithms. In Ronald V. Book, editor, Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, volume 488 of Lecture Notes in Computer Science, pages 162-173. Springer, 1991. URL: https://doi.org/10.1007/3-540-53904-2_94.
  19. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci., 6:223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  20. Sylvain Schmitz. Complexity bounds for ordinal-based termination - (invited talk). In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, volume 8762 of Lecture Notes in Computer Science, pages 1-19. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_1.
  21. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  22. Qizhe Yang and Yuxi Fu. Reachability in 3-vass is in tower. CoRR, abs/2306.05710, 2023. URL: https://doi.org/10.48550/arXiv.2306.05710.
  23. Georg Zetzsche. The complexity of downward closure comparisons. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 123:1-123:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.ICALP.2016.123.
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