Improving Reachability in Vector Addition Systems through Pumpability

TL;DR

This paper improves the theoretical bounds for reachability in vector addition systems by refining pumpability analysis, leading to tighter complexity bounds in fixed dimensions.

Contribution

It introduces a refined pumpability analysis that improves upper bounds for VAS reachability, especially in low dimensions, and simplifies techniques for 2-dimensional cases.

Findings

Established an F_{d-2} upper bound for d-dimensional VAS reachability.

Proved PSPACE upper bound for 4-dimensional VAS reachability.

Proved ELEMENTARY upper bound for 5-dimensional VAS reachability.

Abstract

Vector addition systems (VAS) constitute an important model of computation and concurrency that is equally expressive as the Petri net model. Recently, a lot of research has been conducted on vector addition systems with states (VASS), which are VASes equipped with a finite state control. Results on VASS naturally carry over to VAS, but no straightforward improvement is available. In this paper, we investigate the reachability problem in VAS in fixed dimensions. Based on a pumpability analysis of VAS that refines Rackoff's extraction for VASS, we obtain an F_{d-2} upper bound for the d-dimensional VAS reachability problem, improving the F_d upper bound inherited from the d-dimensional VASS reachability problem. Low-dimensional VASes are also considered. In particular, we establish a PSPACE upper bound for reachability in 4-dimensional VAS and an ELEMENTARY upper bound for 5-dimensional VAS, while the same upper bounds were known only for 2-VASS and 3-VASS, respectively. The result for 4-VAS particularly hinges on a simplified projection technique developed for geometrically 2-dimensional VASSes, whose reachability problem is shown to be equivalent to 2-VASS.