Long Runs Imply Big Separators in Vector Addition Systems

Abstract

Despite recent progress which settled the complexity of the reachability problem for Vector Addition Systems with States (VASSes) as being Ackermann-complete we still lack much understanding for that problem. A striking example is the reachability problem for three-dimensional VASSes (3-VASSes): it is only known to be PSpace-hard and not known to be elementary. One possible approach which turned out to be successful for many VASS subclasses is to prove that to check reachability it suffices to inspect only runs of some bounded length. This approach however has its limitations, it is usually hard to design an algorithm substantially faster than the possible size of finite reachability sets in that VASS subclass. It motivates a search for other techniques, which may be suitable for designing fast algorithms. In 2010 Leroux has proven that non-reachability between two configurations implies separability of the source from the target by some semilinear set, which is an inductive invariant. There can be a reasonable hope that it suffices to look for separators of bounded size, which would deliver an efficient algorithm for VASS reachability. In the paper we show that also this approach meets an obstacle: in VASSes fulfilling some rather natural conditions existence of only long runs between some configurations implies existence of only big separators between some other configurations (and in a slightly modified VASS). Additionally we prove that a few known examples of involved VASSes fulfil the mentioned conditions. Therefore improving the complexity of the reachability problem (for any subclass) using the separators approach may not be simpler than using the short run approach.