Hyper-Ackermannian bounds for pushdown vector addition systems

Authors:
Open Access
Publisher website
Google Scholar
Abstract
Full version of the paper published in the proceedings of CSL-LICS 2014. 14 pages.International audienceThis paper studies the boundedness and termination problems for vector addition systems equipped with one stack. We introduce an algorithm, inspired by the Karp & Miller algorithm, that solves both problems for the larger class of well-structured pushdown systems. We show that the worst-case running time of this algorithm is hyper-Ackermannian for pushdown vector addition systems. For the upper bound, we introduce the notion of bad nested words over a well-quasi-ordered set, and we provide a general scheme of induction for bounding their lengths. We derive from this scheme a hyper-Ackermannian upper bound for the length of bad nested words over vectors of natural numbers. For the lower bound, we exhibit a family of pushdown vector addition systems with finite but large reachability sets (hyper-Ackermannian)

This publication has 18 references indexed in Scilit: