Document Open Access Logo

On Continuous Pushdown VASS in One Dimension

Authors Guillermo A. Pérez , Shrisha Rao

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.34.pdf
  • Filesize: 0.83 MB
  • 20 pages

Document Identifiers

Author Details

Guillermo A. Pérez
  • University of Antwerp – Flanders Make, Antwerp, Belgium
Shrisha Rao
  • University of Antwerp – Flanders Make, Antwerp, Belgium

Funding

Work supported by the Flemish inter-university (iBOF) "DESCARTES" project.

Acknowledgements

We thank Georg Zetzsche for help with the hardness proofs in the model with lower bounds; A. R. Balasubramanian for his comments on an early version of this work, and Tim Leys and Ritam Raha for useful discussions on the topic of (continuous) counter automata.

Cite AsGet BibTex

Guillermo A. Pérez and Shrisha Rao. On Continuous Pushdown VASS in One Dimension. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.34

Abstract

A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown stack. The algorithmic analysis of PVASS has applications such as static analysis of recursive programs manipulating integer variables. Unfortunately, reachability analysis, even for one-dimensional PVASS is not known to be decidable. So, we relax the model of one-dimensional PVASS to make the counter updates continuous and show that in this case reachability, coverability, and boundedness are decidable in polynomial time. In addition, for the extension of the model with lower-bound guards on the states, we show that coverability and reachability are NP-complete, and boundedness is coNP-complete.

Subject Classification

ACM Subject Classification
  • Theory of computation → Grammars and context-free languages
  • Theory of computation → Concurrency
Keywords
  • Vector addition systems
  • Pushdown automata
  • Reachability

Metrics

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

References

  1. A. R. Balasubramanian. Decidability and complexity of decision problems for affine continuous VASS. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 7:1-7:13. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662124.
  2. A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Reachability in continuous pushdown VASS. Proc. ACM Program. Lang., 8(POPL):90-114, 2024. URL: https://doi.org/10.1145/3633279.
  3. Michael Blondin, Christoph Haase, and Philip Offtermatt. Directed reachability for infinite-state systems. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, volume 12652 of Lecture Notes in Computer Science, pages 3-23. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_1.
  4. Michael Blondin, Tim Leys, Filip Mazowiecki, Philip Offtermatt, and Guillermo A. Pérez. Continuous one-counter automata. ACM Trans. Comput. Log., 24(1):3:1-3:31, 2023. URL: https://doi.org/10.1145/3558549.
  5. Dmitry Chistikov and Rupak Majumdar. Unary pushdown automata and straight-line programs. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming, pages 146-157, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. 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. J. ACM, 68(1):7:1-7:28, 2021. URL: https://doi.org/10.1145/3422822.
  7. Matthias Englert, Piotr Hofman, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Juliusz Straszyński. A lower bound for the coverability problem in acyclic pushdown vas. Information Processing Letters, 167:106079, 2021. Google Scholar
  8. Yuval Filmus. Hardness of finding a word of length at most k accepted by a nondeterministic pushdown automaton. https://cstheory.stackexchange.com/questions/4429/hardness-of-finding-a-word-of-length-at-most-k-accepted-by-a-nondeterministic, 2011.
  9. Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche. Reachability in bidirected pushdown VASS. In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, volume 229 of LIPIcs, pages 124:1-124:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.124.
  10. Christoph Haase. A survival guide to presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. Google Scholar
  11. Matthew Hague and Anthony Widjaja Lin. Model checking recursive programs with numeric data types. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 743-759. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_60.
  12. Matthew Hague and Anthony Widjaja Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, volume 7358 of Lecture Notes in Computer Science, pages 260-276. Springer, 2012. Google Scholar
  13. John E. Hopcroft and Jeff D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company, 1979. Google Scholar
  14. Jérôme Leroux, M. Praveen, and Grégoire Sutre. Hyper-ackermannian bounds for pushdown vector addition systems. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 63:1-63:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603146.
  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, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In International Colloquium on Automata, Languages, and Programming, pages 324-336. Springer, 2015. Google Scholar
  17. Sylvain Schmitz. The complexity of reachability in vector addition systems. ACM SIGLOG News, 3(1):4-21, 2016. URL: https://doi.org/10.1145/2893582.2893585.
  18. Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. On the complexity of equational horn clauses. In CADE, volume 3632 of Lecture Notes in Computer Science, pages 337-352. Springer, 2005. 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