On the Boundedness Problem for Pushdown Vector Addition Systems

Jérôme Leroux
Friday, 28 March, 2014 - 14:00
NO Solvay (5th floor)

Vector addition systems (VAS), or equivalently Petri nets, are a well-studied and fundamental model for the analysis of concurrent systems. Despite their fairly large expressive power, many verification problems for VAS are decidable: coverability, boundedness, reachability, liveness, etc. In this work, we study an extension of VAS, called Pushdown VAS, that allows them to use a stack over a finite alphabet. Our main contribution is an algorithm for the boundedness problem together with an analysis of its complexity. This algorithm is based on the well-known Karp-Miller tree for VAS. We show that the worst-case running time of this algorithm is hyper- Ackermannian. (Joint work with G. Sutre and M. Praveen)