2014/12/13 by Michael Blondin, Alain Finkel, Stefan Göller +2 · 3 citations
Computer Science · #cs.FL #cs.CC #cs.LO
paper · pdf · doi:10.1109/lics.2015.14
27 pages, 8 figures
arxiv created 2014/12/13 · arxiv updated 2017/03/20
Determining the complexity of the reachability problem for vector addition systems with states (VASS) is a long-standing open problem in computer science. Long known to be decidable, the problem to this day lacks any complexity upper bound whatsoever. In this paper, reachability for two-dimensional VASS is shown PSPACE-complete. This improves on a previously known doubly exponential time bound established by Howell, Rosier, Huynh and Yen in 1986. The coverability and boundedness problems are also noted to be PSPACE-complete. In addition, some complexity results are given for the reachability problem in two-dimensional VASS and in integer VASS when numbers are encoded in unary.