Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete

TL;DR

This paper proves that the reachability problem for two-dimensional vector addition systems with states (VASS) is PSPACE-complete, resolving a long-standing open problem and improving previous complexity bounds.

Contribution

The paper establishes PSPACE-completeness of reachability in 2D VASS, providing the first tight complexity classification for this problem.

Findings

Reachability in 2D VASS is PSPACE-complete.

Coverability and boundedness are also PSPACE-complete.

Complexity results are extended to unary-encoded numbers in 2D VASS.

Abstract

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.