Long Runs Imply Big Separators in Vector Addition Systems

TL;DR

This paper investigates the relationship between long runs and large separators in Vector Addition Systems, showing that certain natural conditions imply the necessity of big separators, which limits the effectiveness of separator-based algorithms for reachability.

Contribution

It demonstrates that in some VASS subclasses, long runs imply large separators, highlighting limitations of separator-based approaches for reachability analysis.

Findings

Long runs imply big separators in certain VASS subclasses.

Separator-based methods may not be more efficient than short run approaches.

Examples of VASSes fulfilling the natural conditions are provided.

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.