The Reachability Problem for Two-Dimensional Vector Addition Systems with States

Patrick Totzke

Does a given regular language over an alphabet of integer vectors contain a word such that

  1. the sum of every prefix is non-negative and
  2. the sum of the whole word is 0 ?
This problem, known as the reachability problem for vector addition systems with states, has widespread applications in logic, formal languages, control theory, and the verification of concurrent processes. It was first shown to be decidable already in the early 80s, but its exact complexity remains elusive to date.

In this talk I will recall the status quo regarding the complexity of the reachability problem, mostly focussing on the subproblems for fixed and small dimensions.

I will present our recent result on the two-dimensional case that the length of shortest reachability certificates is polynomial in the largest integer and the size of the NFA defining the input language. This complements a result by Blondin et. al. (LICS'15) and shows that the 2-dim. reachability problem is PSPACE-complete when numbers are encoded in binary and NL-complete if the input is given in unary.