文章基本信息

标题：On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems
本地全文：下载
作者：Vincent Penelle ; Sylvain Salvati ; Gr{\'e}goire Sutre 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：122
页码：1-20
DOI：10.4230/LIPIcs.FSTTCS.2018.44
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Higher-order pushdown automata; Vector addition systems; Boundedness problem; Termination problem; Coverability problem