Reachability in Continuous Pushdown VASS
Authors: 
A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, Georg ZetzscheAuthors Info & Claims
Article No.: 4, Pages 90 - 114
Abstract
Pushdown Vector Addition Systems with States (PVASS) consist of finitely many control states, a pushdown stack, and a set of counters that can be incremented and decremented, but not tested for zero. Whether the reachability problem is decidable for PVASS is a long-standing open problem. We consider continuous PVASS, which are PVASS with a continuous semantics. This means, the counter values are rational numbers and whenever a vector is added to the current counter values, this vector is first scaled with an arbitrarily chosen rational factor between zero and one. We show that reachability in continuous PVASS is NEXPTIME-complete. Our result is unusually robust: Reachability can be decided in NEXPTIME even if all numbers are specified in binary. On the other hand, NEXPTIME-hardness already holds for coverability, in fixed dimension, for bounded stack, and even if all numbers are specified in unary.
References
[1]
C. Aiswarya, Soumodev Mal, and Prakash Saivasan. 2022. On the Satisfiability of Context-free String Constraints with Subword-Ordering. In LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, Christel Baier and Dana Fisman (Eds.). ACM, 6:1–6:13. https://doi.org/10.1145/3531130.3533329
[2]
Rajeev Alur, Michael Benedikt, Kousha Etessami, Patrice Godefroid, Thomas W. Reps, and Mihalis Yannakakis. 2005. Analysis of recursive state machines. ACM Trans. Program. Lang. Syst., 27, 4 (2005), 786–818. https://doi.org/10.1145/1075382.1075387
[3]
Rajeev Alur, Ashutosh Trivedi, and Dominik Wojtczak. 2012. Optimal scheduling for constant-rate multi-mode systems. In Hybrid Systems: Computation and Control (part of CPS Week 2012), HSCC’12, Beijing, China, April 17-19, 2012, Thao Dang and Ian M. Mitchell (Eds.). ACM, 75–84. https://doi.org/10.1145/2185632.2185647
[4]
Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. 2009. Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. In Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, Stefan Kowalewski and Anna Philippou (Eds.) (Lecture Notes in Computer Science, Vol. 5505). Springer, 107–123. https://doi.org/10.1007/978-3-642-00768-2_11
[5]
Mohamed Faouzi Atig and Pierre Ganty. 2011. Approximating Petri Net Reachability Along Context-free Traces. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), Supratik Chakraborty and Amit Kumar (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 13). Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 152–163. isbn:978-3-939897-34-7 issn:1868-8969 https://doi.org/10.4230/LIPIcs.FSTTCS.2011.152
[6]
A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. 2023. Reachability in Continuous Pushdown VASS. arXiv, arxiv:2310.16798
[7]
Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. 2023. Context-Bounded Verification of Context-Free Specifications. Proc. ACM Program. Lang., 7, POPL (2023), 2141–2170. https://doi.org/10.1145/3571266
[8]
Jean Berstel. 1979. Transductions and context-free languages. Teubner, Stuttgart.
[9]
Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. 2016. Approaching the Coverability Problem Continuously. In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-François Raskin (Eds.) (Lecture Notes in Computer Science). Springer, Berlin, Heidelberg. 480–496. https://doi.org/10.1007/978-3-662-49674-9_28
[10]
Michael Blondin and Christoph Haase. 2017. Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, Reykjavik, Iceland. 1–12. isbn:978-1-5090-3018-7 https://doi.org/10.1109/LICS.2017.8005068
[11]
Swarat Chaudhuri. 2008. Subcubic algorithms for recursive state machines. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, George C. Necula and Philip Wadler (Eds.). ACM, 159–169. https://doi.org/10.1145/1328438.1328460
[12]
Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Warren A. Hunt Jr. and Fabio Somenzi (Eds.) (Lecture Notes in Computer Science, Vol. 2725). Springer, 420–432. https://doi.org/10.1007/978-3-540-45069-6_39
[13]
Wojciech Czerwiński and Ł ukasz Orlikowski. 2022. Reachability in Vector Addition Systems Is Ackermann-complete. In 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). 1229–1240. issn:2575-8454 https://doi.org/10.1109/FOCS52979.2021.00120
[14]
René David. 1987. Continuous Petri nets. In Proc. 8th European Workshop on Appli. & Theory of Petri nets, 1987.
[15]
Matthias Englert, Piotr Hofman, Sł awomir Lasota, Ranko Lazić, Jérôme Leroux, and Juliusz Straszyński. 2021. A Lower Bound for the Coverability Problem in Acyclic Pushdown VAS. Inform. Process. Lett., 167 (2021), April, 106079. issn:0020-0190 https://doi.org/10.1016/j.ipl.2020.106079
[16]
Javier Esparza, Pierre Ganty, Stefan Kiefer, and Michael Luttenberger. 2011. Parikh’s theorem: A simple and direct automaton construction. Inf. Process. Lett., 111, 12 (2011), 614–619. https://doi.org/10.1016/j.ipl.2011.03.019
[17]
Estíbaliz Fraca and Serge Haddad. 2015. Complexity analysis of continuous Petri nets. Fundamenta informaticae, 137, 1 (2015), 1–28.
[18]
Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche. 2022. Reachability in Bidirected Pushdown VASS. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022), Mikoł aj Bojańczyk, Emanuela Merelli, and David P. Woodruff (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 229). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 124:1–124:20. isbn:978-3-95977-235-8 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ICALP.2022.124
[19]
Michel Henri Théodore Hack. 1976. Decidability questions for Petri Nets. Ph. D. Dissertation. Massachusetts Institute of Technology.
[20]
Richard M. Karp and Raymond E. Miller. 1969. Parallel Program Schemata. J. Comput. System Sci., 3, 2 (1969), May, 147–195. issn:0022-0000 https://doi.org/10.1016/S0022-0000(69)80011-5
[21]
Adam Husted Kjelstrøm and Andreas Pavlogiannis. 2022. The decidability and complexity of interleaved bidirected Dyck reachability. Proc. ACM Program. Lang., 6, POPL (2022), 1–26. https://doi.org/10.1145/3498673
[22]
Jérôme Leroux. 2022. The reachability problem for Petri nets is not primitive recursive. In 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). 1241–1252.
[23]
Jérôme Leroux and Sylvain Schmitz. 2019. 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. IEEE, 1–13. https://doi.org/10.1109/LICS.2019.8785796
[24]
Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. 2015. On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension. In Automata, Languages, and Programming, Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Eds.). 9135, Springer Berlin Heidelberg, Berlin, Heidelberg. 324–336. isbn:978-3-662-47665-9 978-3-662-47666-6 https://doi.org/10.1007/978-3-662-47666-6_26
[25]
Yuanbo Li, Qirun Zhang, and Thomas W. Reps. 2021. On the complexity of bidirected interleaved Dyck-reachability. Proc. ACM Program. Lang., 5, POPL (2021), 1–28. https://doi.org/10.1145/3434340
[26]
Markus Lohrey, Andreas Rosowski, and Georg Zetzsche. 2022. Membership Problems in Finite Groups. In 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, Stefan Szeider, Robert Ganian, and Alexandra Silva (Eds.) (LIPIcs, Vol. 241). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 71:1–71:16. https://doi.org/10.4230/LIPICS.MFCS.2022.71
[27]
Christos H. Papadimitriou. 2007. Computational complexity. Academic Internet Publ. isbn:978-1-4288-1409-7
[28]
Charles Rackoff. 1978. The Covering and Boundedness Problems for Vector Addition Systems. Theor. Comput. Sci., 6 (1978), 223–231. https://doi.org/10.1016/0304-3975(78)90036-1
[29]
Klaus Reinhardt. 2008. Reachability in Petri nets with inhibitor arcs. Electronic Notes in Theoretical Computer Science, 223 (2008), 239–264.
[30]
Thomas W. Reps, Susan Horwitz, and Shmuel Sagiv. 1995. Precise Interprocedural Dataflow Analysis via Graph Reachability. In Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, Ron K. Cytron and Peter Lee (Eds.). ACM Press, 49–61. https://doi.org/10.1145/199448.199462
[31]
Thomas W. Reps, Emma Turetsky, and Prathmesh Prabhu. 2016. Newtonian program analysis via tensor product. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 663–677. https://doi.org/10.1145/2837614.2837659
[32]
Arnold L Rosenberg. 1967. A machine realization of the linear context-free languages. Information and Control, 10, 2 (1967), 175–188. https://doi.org/10.1016/S0019-9958(67)80006-8
[33]
Louis E. Rosier and Hsu-Chun Yen. 1986. A Multiparameter Analysis of the Boundedness Problem for Vector Addition Systems. J. Comput. Syst. Sci., 32, 1 (1986), 105–135. https://doi.org/10.1016/0022-0000(86)90006-1
[34]
Sylvain Schmitz and Georg Zetzsche. 2019. Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets. In 13th International Conference on Reachability Problems (RP 2019), Emmanuel Filiot, Raphaël Jungers, and Igor Potapov (Eds.) (Lecture Notes in Computer Science, Vol. 11674). Springer International Publishing, Brussels, Belgium. 193–201. https://doi.org/10.1007/978-3-030-30806-3_15
[35]
Michael Sipser. 2012. Introduction to the Theory of Computation. Cengage Learning. isbn:978-1-133-18781-3 lccn:2012938665
[36]
Eduardo D. Sontag. 1985. Real Addition and the Polynomial Hierarchy. Inform. Process. Lett., 20, 3 (1985), April, 115–120. issn:00200190 https://doi.org/10.1016/0020-0190(85)90076-6
[37]
Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. 2010. From program verification to program synthesis. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 313–326. https://doi.org/10.1145/1706299.1706337
[38]
Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. 2005. On the Complexity of Equational Horn Clauses. In Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, Robert Nieuwenhuis (Ed.) (Lecture Notes in Computer Science, Vol. 3632). Springer, 337–352. https://doi.org/10.1007/11532231_25
[39]
Mihalis Yannakakis. 1990. Graph-Theoretic Methods in Database Theory. In Proceedings of the Ninth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, April 2-4, 1990, Nashville, Tennessee, USA. ACM Press, 230–242.
Index Terms
- Reachability in Continuous Pushdown VASS
Recommendations
Decidability and Complexity of Decision Problems for Affine Continuous VASS
LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer ScienceVector addition system with states (VASS) is a popular model for the verification of concurrent systems. VASS consists of finitely many control states and a set of counters which can be incremented and decremented, but not tested for zero. VASS is a ...
Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems
Timed-register pushdown automata constitute a very expressive class of automata, whose transitions may involve state, input, and top-of-stack timed registers with unbounded differences. They strictly subsume pushdown timed automata of Bouajjani et al., ...
On the complexity of membership and counting in height-deterministic pushdown automata
Visibly pushdown languages properly generalize regular languages and are properly contained in deterministic context-free languages. The complexity of their membership problem is equivalent to that of regular languages. However, the corresponding ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2024
2820 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 05 January 2024
Published in PACMPL Volume 8, Issue POPL
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 383Total Downloads
- Downloads (Last 12 months)383
- Downloads (Last 6 weeks)47
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in