Document Open Access Logo

Reachability in Bidirected Pushdown VASS

Authors Moses Ganardi , Rupak Majumdar , Andreas Pavlogiannis , Lia Schütze , Georg Zetzsche

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.124.pdf
  • Filesize: 0.86 MB
  • 20 pages

Document Identifiers

Author Details

Moses Ganardi
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Rupak Majumdar
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Andreas Pavlogiannis
  • Aarhus University, Denmark
Lia Schütze
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Georg Zetzsche
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Cite AsGet BibTex

Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche. Reachability in Bidirected Pushdown VASS. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 124:1-124:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ICALP.2022.124

Abstract

A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be bidirected if every transition (pushing/popping a symbol or modifying a counter) has an accompanying opposite transition that reverses the effect. Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachability. We show that the reachability problem for bidirected PVASS is decidable in Ackermann time and primitive recursive for any fixed dimension. For the special case of one-dimensional bidirected PVASS, we show reachability is in PSPACE, and in fact in polynomial time if the stack is polynomially bounded. Our results are in contrast to the directed setting, where decidability of reachability is a long-standing open problem already for one dimensional PVASS, and there is a PSPACE-lower bound already for one-dimensional PVASS with bounded stack. The reachability relation in the bidirected (stateless) case is a congruence over ℕ^d. Our upper bounds exploit saturation techniques over congruences. In particular, we show novel elementary-time constructions of semilinear representations of congruences generated by finitely many vector pairs. In the case of one-dimensional PVASS, we employ a saturation procedure over bounded-size counters. We complement our upper bound with a TOWER-hardness result for arbitrary dimension and k-EXPSPACE hardness in dimension 2k+6 using a technique by Lazić and Totzke to implement iterative exponentiations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • Vector addition systems
  • Pushdown
  • Reachability
  • Decidability
  • Complexity

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 IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India, volume 13 of LIPIcs, pages 152-163. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2011.152.
  2. Thomas Becker, Volker Weispfenning, and Heinz Kredel. Gröbner bases - a computational approach to commutative algebra, volume 141 of Graduate texts in mathematics. Springer, 1993. Google Scholar
  3. Rémi Bonnet. Theory of well-structured transition systems and extended vector-addition systems. PhD thesis, ENS Cachan, France, 2013. Thèse de doctorat. Google Scholar
  4. Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun. Model checking vector addition systems with one zero-test. Log. Methods Comput. Sci., 8(2), 2012. URL: https://doi.org/10.2168/LMCS-8(2:11)2012.
  5. Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR '97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings, volume 1243 of Lecture Notes in Computer Science, pages 135-150. Springer, 1997. URL: https://doi.org/10.1007/3-540-63141-0_10.
  6. Zakaria Bouziane and Alain Finkel. Cyclic Petri net reachability sets are semi-linear effectively constructible. In Second International Workshop on Verification of Infinite State Systems, Infinity 1997, Bologna, Italy, July 11-12, 1997, volume 9 of Electronic Notes in Theoretical Computer Science, pages 15-24. Elsevier, 1997. URL: https://doi.org/10.1016/S1571-0661(05)80423-2.
  7. Bruno Buchberger. Ein Algorithmus zum Auffinden der Basiselemente des Restklassenrings nach einem nulldimensionalen Polynomideal. PhD thesis, Universität Innsbruck, 1965. Google Scholar
  8. Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. Proc. ACM Program. Lang., 2(POPL), December 2018. URL: https://doi.org/10.1145/3158118.
  9. Swarat Chaudhuri. 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, pages 159-169. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328460.
  10. David C Cooper. Theorem proving in arithmetic without multiplication. Machine intelligence, 7(91-99):300, 1972. Google Scholar
  11. Wojciech Czerwiński, Slawomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019, pages 24-33. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316369.
  12. Wojciech Czerwiński and Łukasz 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.
  13. Thomas W Dubé. The structure of polynomial ideals and Gröbner bases. SIAM Journal on Computing, 19(4):750-773, 1990. URL: https://doi.org/10.1137/0219053.
  14. Samuel Eilenberg and M. P. Schützenberger. Rational sets in commutative monoids. Journal of Algebra, 13(2):173-191, 1969. URL: https://doi.org/10.1016/0021-8693(69)90070-2.
  15. Matthias Englert, Piotr Hofman, Slawomir Lasota, Ranko Lazić, Jérôme Leroux, and Juliusz Straszynski. A lower bound for the coverability problem in acyclic pushdown VAS. Inf. Process. Lett., 167:106079, 2021. URL: https://doi.org/10.1016/j.ipl.2020.106079.
  16. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and Primitive-Recursive Bounds with Dickson’s Lemma. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 269-278. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.39.
  17. Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for two-counter machines with one test and one reset. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India, volume 122 of LIPIcs, pages 31:1-31:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.31.
  18. Alain Finkel and Grégoire Sutre. Decidability of reachability problems for classes of two counters automata. In STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Lille, France, February 2000, Proceedings, volume 1770 of Lecture Notes in Computer Science, pages 346-357. Springer, 2000. URL: https://doi.org/10.1007/3-540-46541-3_29.
  19. Patrick C. Fischer, Albert R. Meyer, and Arnold L. Rosenberg. Counter machines and counter languages. Mathematical systems theory, 1968. URL: https://doi.org/10.1007/BF01694011.
  20. Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche. Reachability in bidirected pushdown VASS. Full version of this paper. URL: http://arxiv.org/abs/2204.11799.
  21. Moses Ganardi, Rupak Majumdar, and Georg Zetzsche. The complexity of bidirected reachability in valence systems. To appear in Proc. of the Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022). URL: http://arxiv.org/abs/2110.03654.
  22. Jan Grabowski. An algorithm to identify slices, with applications to vector replacement systems. In International Conference on Fundamentals of Computation Theory (FCT 1981), pages 425-432. Springer, 1981. URL: https://doi.org/10.1007/3-540-10854-8_46.
  23. Christoph Haase. A survival guide to Presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. URL: https://doi.org/10.1145/3242953.3242964.
  24. Matthew Hague and Anthony Widjaja Lin. Model checking recursive programs with numeric data types. In 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.
  25. Tero Harju, Oscar H. Ibarra, Juhani Karhumäki, and Arto Salomaa. Some decision problems concerning semilinearity and commutation. J. Comput. Syst. Sci., 65(2):278-294, 2002. URL: https://doi.org/10.1006/jcss.2002.1836.
  26. Nevin Heintze and David A. McAllester. On the cubic bottleneck in subtyping and flow analysis. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science (LICS), Warsaw, Poland, June 29 - July 2, 1997, pages 342-351. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614960.
  27. Yoram Hirshfeld. Congruences in commutative semigroups. LFCS, Department of Computer Science, University of Edinburgh Edinburgh, 1994. Google Scholar
  28. John E Hopcroft and Jeffrey D Ullman. Introduction to Automata Theory, Languages and Computation. Adison-Wesley, Reading, Mass, 1979. Google Scholar
  29. Dung T. Huynh. A superexponential lower bound for Gröbner bases and Church-Rosser commutative Thue systems. Inf. Control., 68(1-3):196-206, 1986. URL: https://doi.org/10.1016/S0019-9958(86)80035-3.
  30. Jarkko Kari. Reversible cellular automata: From fundamental classical results to recent developments. New Gener. Comput., 36(3):145-172, 2018. URL: https://doi.org/10.1007/s00354-018-0034-6.
  31. Adam Husted Kjelstrøm and Andreas Pavlogiannis. The decidability and complexity of interleaved bidirected Dyck reachability. Proc. ACM Program. Lang., 6(POPL):1-26, 2022. URL: https://doi.org/10.1145/3498673.
  32. Ulla Koppenhagen and Ernst W. Mayr. The complexity of the coverability, the containment, and the equivalence problems for commutative semigroups. In Fundamentals of Computation Theory, 11th International Symposium, FCT '97, Kraków, Poland, September 1-3, 1997, Proceedings, volume 1279 of Lecture Notes in Computer Science, pages 257-268. Springer, 1997. URL: https://doi.org/10.1007/BFb0036189.
  33. Ranko Lazić and Patrick Totzke. What Makes Petri Nets Harder to Verify: Stack or Data?, pages 144-161. Springer International Publishing, 2017. URL: https://doi.org/10.1007/978-3-319-51046-0_8.
  34. Jérôme Leroux. Vector addition system reachability problem: a short self-contained proof. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 307-316. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926421.
  35. Jérôme Leroux. Vector addition system reversible reachability problem. Log. Methods Comput. Sci., 9(1), 2013. URL: https://doi.org/10.2168/LMCS-9(1:5)2013.
  36. Jérôme Leroux. Distance between mutually reachable Petri net configurations. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, volume 150 of LIPIcs, pages 47:1-47:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2019.47.
  37. 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.
  38. 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.
  39. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 324-336. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_26.
  40. Yuanbo Li, Qirun Zhang, and Thomas W. Reps. Fast graph simplification for interleaved Dyck-reachability. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 780-793. ACM, 2020. URL: https://doi.org/10.1145/3385412.3386021.
  41. Yuanbo Li, Qirun Zhang, and Thomas W. Reps. On the complexity of bidirected interleaved Dyck-reachability. Proc. ACM Program. Lang., 5(POPL):1-28, 2021. URL: https://doi.org/10.1145/3434340.
  42. Markus Lohrey and Benjamin Steinberg. An automata theoretic approach to the generalized word problem in graphs of groups. Proceedings of the American Mathematical Society, 138(2):445-453, 2010. URL: https://doi.org/10.1090/S0002-9939-09-10126-0.
  43. Ernst W. Mayr and Albert R. Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in mathematics, 46(3):305-329, 1982. URL: https://doi.org/10.1016/0001-8708(82)90048-2.
  44. Derek C. Oppen. A 2^2^2^pn upper bound on the complexity of Presburger arithmetic. J. Comput. Syst. Sci., 16(3):323-332, 1978. URL: https://doi.org/10.1016/0022-0000(78)90021-1.
  45. Laurent Pierre. Rational indexes of generators of the cone of context-free languages. Theoretical Computer Science, 95(2):279-305, 1992. URL: https://doi.org/10.1016/0304-3975(92)90269-L.
  46. Emil L. Post. Recursive unsolvability of a problem of Thue. J. Symb. Log., 12(1):1-11, 1947. URL: https://doi.org/10.2307/2267170.
  47. Klaus Reinhardt. Reachability in Petri nets with inhibitor arcs. Electron. Notes Theor. Comput. Sci., 223:239-264, 2008. URL: https://doi.org/10.1016/j.entcs.2008.12.042.
  48. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  49. Sylvain Schmitz. Algorithmic Complexity of Well-Quasi-Orders. (Complexité algorithmique des beaux pré-ordres). Habilitation thesis, École normale supérieure Paris-Saclay, 2017. URL: https://tel.archives-ouvertes.fr/tel-01663266.
  50. Sylvain Schmitz and Georg Zetzsche. Coverability is undecidable in one-dimensional pushdown vector addition systems with resets. In Reachability Problems - 13th International Conference, RP 2019, Brussels, Belgium, September 11-13, 2019, Proceedings, volume 11674 of Lecture Notes in Computer Science, pages 193-201. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30806-3_15.
  51. Guoqing Xu, Atanas Rountev, and Manu Sridharan. Scaling CFL-reachability-based points-to analysis using context-sensitive must-not-alias analysis. In ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genoa, Italy, July 6-10, 2009. Proceedings, volume 5653 of Lecture Notes in Computer Science, pages 98-122. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03013-0_6.
  52. Dacong Yan, Guoqing Xu, and Atanas Rountev. Demand-driven context-sensitive alias analysis for Java. In Proceedings of the 20th International Symposium on Software Testing and Analysis, ISSTA 2011, Toronto, ON, Canada, July 17-21, 2011, pages 155-165. ACM, 2011. URL: https://doi.org/10.1145/2001420.2001440.
  53. Georg Zetzsche. The emptiness problem for valence automata over graph monoids. Information and Computation, 277, 2021. URL: https://doi.org/10.1016/j.ic.2020.104583.
  54. Qirun Zhang, Michael R. Lyu, Hao Yuan, and Zhendong Su. Fast algorithms for Dyck-CFL-reachability with applications to alias analysis. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pages 435-446. ACM, 2013. URL: https://doi.org/10.1145/2491956.2462159.
  55. Qirun Zhang and Zhendong Su. Context-sensitive data-dependence analysis via linear conjunctive language reachability. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 344-358. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009848.
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