Document Open Access Logo

On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems

Authors Vincent Penelle, Sylvain Salvati, Grégoire Sutre

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.44.pdf
  • Filesize: 0.64 MB
  • 20 pages

Document Identifiers

Author Details

Vincent Penelle
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux-INP, Talence, France
Sylvain Salvati
  • CRIStAL, Univ. Lille, INRIA, Lille, France
Grégoire Sutre
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux-INP, Talence, France

Funding

This work was supported by the grant ANR-17-CE40-0028 of the French National Research Agency ANR (project BRAVAS).

Cite AsGet BibTex

Vincent Penelle, Sylvain Salvati, and Grégoire Sutre. On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 44:1-44:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSTTCS.2018.44

Abstract

Karp and Miller's algorithm is a well-known decision procedure that solves the termination and boundedness problems for vector addition systems with states (VASS), or equivalently Petri nets. This procedure was later extended to a general class of models, well-structured transition systems, and, more recently, to pushdown VASS. In this paper, we extend pushdown VASS to higher-order pushdown VASS (called HOPVASS), and we investigate whether an approach à la Karp and Miller can still be used to solve termination and boundedness. We provide a decidable characterisation of runs that can be iterated arbitrarily many times, which is the main ingredient of Karp and Miller's approach. However, the resulting Karp and Miller procedure only gives a semi-algorithm for HOPVASS. In fact, we show that coverability, termination and boundedness are all undecidable for HOPVASS, even in the restricted subcase of one counter and an order 2 stack. On the bright side, we prove that this semi-algorithm is in fact an algorithm for higher-order pushdown automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Logic and verification
Keywords
  • Higher-order pushdown automata
  • Vector addition systems
  • Boundedness problem
  • Termination problem
  • Coverability problem

Metrics

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

References

  1. Alfred V. Aho. Nested Stack Automata. J. ACM, 16(3):383-406, 1969. URL: http://dx.doi.org/10.1145/321526.321529.
  2. Arnaud Carayol. Regular Sets of Higher-Order Pushdown Stacks. In Joanna Jedrzejowicz and Andrzej Szepietowski, editors, Mathematical Foundations of Computer Science 2005, 30th International Symposium, MFCS 2005, Gdansk, Poland, August 29 - September 2, 2005, Proceedings, volume 3618 of Lecture Notes in Computer Science, pages 168-179. Springer, 2005. URL: http://dx.doi.org/10.1007/11549345_16.
  3. Arnaud Carayol. Automates infinis, logiques et langages. PhD thesis, University of Rennes 1, France, 2006. URL: https://tel.archives-ouvertes.fr/tel-00628513.
  4. Arnaud Carayol and Stefan Wöhrle. The Caucal Hierarchy of Infinite Graphs in Terms of Logic and Higher-Order Pushdown Automata. In Paritosh K. Pandya and Jaikumar Radhakrishnan, editors, FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 23rd Conference, Mumbai, India, December 15-17, 2003, Proceedings, volume 2914 of Lecture Notes in Computer Science, pages 112-123. Springer, 2003. URL: http://dx.doi.org/10.1007/978-3-540-24597-1_10.
  5. Didier Caucal. On Infinite Terms Having a Decidable Monadic Theory. In Krzysztof Diks and Wojciech Rytter, editors, Mathematical Foundations of Computer Science 2002, 27th International Symposium, MFCS 2002, Warsaw, Poland, August 26-30, 2002, Proceedings, volume 2420 of Lecture Notes in Computer Science, pages 165-176. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-45687-2_13.
  6. Alain Finkel. A Generalization of the Procedure of Karp and Miller to Well Structured Transition Systems. In Thomas Ottmann, editor, Automata, Languages and Programming, 14th International Colloquium, ICALP87, Karlsruhe, Germany, July 13-17, 1987, Proceedings, volume 267 of Lecture Notes in Computer Science, pages 499-508. Springer, 1987. URL: http://dx.doi.org/10.1007/3-540-18088-5_43.
  7. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. URL: http://dx.doi.org/10.1016/S0304-3975(00)00102-X.
  8. Sheila A. Greibach. Full AFLs and Nested Iterated Substitution. Information and Control, 16(1):7-35, 1970. URL: http://dx.doi.org/10.1016/S0019-9958(70)80039-0.
  9. Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong. Unboundedness and downward closures of higher-order pushdown automata. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 151-163. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837627.
  10. Richard M. Karp and Raymond E. Miller. Parallel Program Schemata. J. Comput. Syst. Sci., 3(2):147-195, 1969. URL: http://dx.doi.org/10.1016/S0022-0000(69)80011-5.
  11. Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Higher-Order Pushdown Trees Are Easy. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 205-222. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-45931-6_15.
  12. Ranko Lazic. The reachability problem for vector addition systems with a stack is not elementary. CoRR, abs/1310.1767, 2013. Presented at RP'12. URL: http://arxiv.org/abs/1310.1767.
  13. Ranko Lazic and Patrick Totzke. What Makes Petri Nets Harder to Verify: Stack or Data? In Thomas Gibson-Robinson, Philippa J. Hopcroft, and Ranko Lazic, editors, Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, volume 10160 of Lecture Notes in Computer Science, pages 144-161. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-51046-0_8.
  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: http://dx.doi.org/10.1145/2603088.2603146.
  15. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On Boundedness Problems for Pushdown Vector Addition Systems. In Mikolaj Bojanczyk, Slawomir Lasota, and Igor Potapov, editors, Reachability Problems - 9th International Workshop, RP 2015, Warsaw, Poland, September 21-23, 2015, Proceedings, volume 9328 of Lecture Notes in Computer Science, pages 101-113. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-24537-9_10.
  16. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, 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: http://dx.doi.org/10.1007/978-3-662-47666-6_26.
  17. Richard J. Lipton. The reachability problem requires exponential space. Technical Report 63, Yale University, January 1976. Google Scholar
  18. A.N. Maslov. Multilevel Stack Automata. Probl. Inf. Transm., 12(1):38-43, 1976. Google Scholar
  19. Ernst W. Mayr and Albert R. Meyer. The Complexity of the Finite Containment Problem for Petri Nets. J. ACM, 28(3):561-576, 1981. URL: http://dx.doi.org/10.1145/322261.322271.
  20. Ken McAloon. Petri nets and large finite sets. Theor. Comput. Sci., 32:173-183, 1984. URL: http://dx.doi.org/10.1016/0304-3975(84)90029-X.
  21. Pawel Parys. A Pumping Lemma for Pushdown Graphs of Any Level. In Christoph Dürr and Thomas Wilke, editors, 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, volume 14 of LIPIcs, pages 54-65. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2012.54.
  22. Charles Rackoff. The Covering and Boundedness Problems for Vector Addition Systems. Theor. Comput. Sci., 6:223-231, 1978. URL: http://dx.doi.org/10.1016/0304-3975(78)90036-1.
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