Reachability in binary 3-VASS is in ExpSpace

We consider the reachability problem for Vector Addition Systems with States (VASS) in dimension three. In the dimension two the problem is known to be PSpace-complete since 2015. However, already for three-dimensional VASS (3-VASS) there is a huge gap in understanding of the complexity and currently the problem is only known to be PSpace-hard and in Tower. We show that the reachability problem in binary 3-VASS (a 3-VASS with numbers on transitions encoded in binary) can be decided in exponential space. This does not fix the complexity, but substantially improves the upper bound. Our main contribution states that if there is a path between two its configurations then there is also a path of at most doubly-exponential length, which immediately implies an ExpSpace algorithm. It is challenging to obtain below-Tower complexity as there exists 3-VASS of finite, but almost Tower-big reachability sets (concretely speaking k-fold exponential, for any k ∈ N). We introduce a novel technique of sandwiching reachability sets between two semilinear sets, which have small representation and behave similarly. This intuitively allows us to deal with big, finite sets in time faster than their size. We also make use of recent results about the form of reachability paths in 2-VASS, sequential cones and other techniques. The presentation is based on a joint work with Ismael Jecker, Sławomir Lasota and Łukasz Orlikowski.

Authors

• Wojciech Czerwiński

Keywords

No keywords are indexed for this paper.