Reachability in five dimensional vector addition systems is pspace complete

Reachability in Five-Dimensional Vector Addition Systems Is PSPACE-Complete

Formal Languages and Automata TheoryComputational Complexity

Summary

The paper studies a type of mathematical model called vector addition systems (VAS), which represent certain computer processes with counters that can only hold nonnegative numbers. The authors focus on VAS with five counters and show that determining whether a particular state can be reached is a problem that is as hard as the well-known PSPACE-complete problems when numbers are recorded in binary. They prove this by demonstrating that if a state is reachable, there is a proof (or witness) of this fact that is not too long, measured in terms of the size of the input. This improves over previous knowledge, which only had very large, non-elementary bounds for this problem.

What this means in practice

  • For concurrent system designers: Use the PSPACE characterization of 5-counter systems to optimize verification tools for concurrent process models.
  • For formal verification engineers: Improve automated verification frameworks by leveraging the polynomial witness bounds for reachability in five-dimensional vector addition systems.

A theory result. No direct application yet.

Authors

Weijun Chen, Bo Fu, Yuxi Fu

Abstract

Vector addition systems (VAS) are a fundamental model of concurrent computation in which transitions update nonnegative integer counters by adding integer vectors, provided all counters remain nonnegative. Closely related to Petri nets, VAS are the single-state counterpart of vector addition systems with states (VASS), which use finitely many states to restrict the available transitions. A classical simulation of $d$-VASS by $(d+3)$-VAS connects their reachability problems, but the complexity-theoretic picture of fixed-dimensional VAS remains largely unclear. While reachability in $2$-VASS is PSPACE-complete under binary encoding, the best known upper bound for $5$-VAS was only elementary. We prove that every reachable $5$-VAS instance has a reachability witness of length polynomial in its unary size. Consequently, $5$-VAS reachability is NL-complete under unary encoding and PSPACE-complete under binary encoding. We also establish a polynomial factorization of the reachability relation of every $d$-VAS with $d \ge 3$. For $5$-VAS, this strengthens Hopcroft and Pansiot's effective semilinearity of reachability sets to the full reachability relation. For every fixed $d\ge3$, it also yields an $\mathsf F_d$ upper bound for reachability in $(d+3)$-VAS.
View PDFOpen arXiv