2026-07-23T05:28:39Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9943 2024-03-06T10:45:10Z ddc:004 open_access

On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems Penelle, Vincent Salvati, Sylvain Sutre, Grégoire Higher-order pushdown automata Vector addition systems Boundedness problem Termination problem Coverability problem 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Vincent Penelle and Sylvain Salvati and Grégoire Sutre 2018 Is Part Of LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2018.44 urn:nbn:de:0030-drops-99432 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.44 eng https://creativecommons.org/licenses/by/3.0/legalcode