Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete

Author

Blondin, Michael ; Finkel, Alain ; Goller, Stefan ; Haase, Christoph ; McKenzie, Pierre

Author_Institution

DIRO, Univ. de Montreal, Montreal, QC, Canada

fYear

2015

fDate

6-10 July 2015

Firstpage

32

Lastpage

43

Abstract

Known to be decidable since 1981, there still remains a huge gap between the best known lower and upper bounds for the reach ability problem for vector addition systems with states (VASS). Here the problem is shown PSPACE-complete in the two-dimensional case, vastly improving on the doubly exponential time bound established in 1986 by Howell, Rosier, Huynh and Yen. Cover ability and bounded ness for two-dimensional VASS are also shown PSPACE-complete, and reach ability in two-dimensional VASS and in integer VASS under unary encoding are considered.

Keywords

computational complexity; decidability; reachability analysis; PSPACE-complete problem; boundedness; coverability; doubly-exponential time bound improvement; integer VASS; lower bounds; reachability problem; two-dimensional VASS; two-dimensional vector addition system-with-states; unary encoding; upper bounds; Automata; Complexity theory; Encoding; Petri nets; Polynomials; Radiation detectors; Upper bound; Parikh images; bounded regular languages; reachability; semi-linear sets; vector addition systems with states;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on

Conference_Location

Kyoto

ISSN

1043-6871

Type

conf

DOI

10.1109/LICS.2015.14

Filename

7174868