Pushdown Vector Addition Systems

In this presentation, we overview classical results about vector addition systems, and we present the boundedness and termination problems for vector addition systems equipped with one stack. We then introduce an algorithm, inspired by the Karp & Miller algorithm, that solves both problems. We show that the worst-case running time of this algorithm is hyper-Ackermannian. This is a joint work with M. Praveen, Grégoire Sutre and Patrick Totzke.