Vector Addition System Reversible Reachability Problem

TL;DR

This paper proves that the reversible reachability problem for vector addition systems is EXPSPACE-complete, providing a complexity classification and characterizing reversibility domains within these systems.

Contribution

It establishes the EXPSPACE-completeness of the reversible reachability problem and characterizes reversibility domains in vector addition systems.

Findings

Reversible reachability is EXPSPACE-complete.

Characterization of reversibility domains.

Provides complexity bounds for the problem.

Abstract

The reachability problem for vector addition systems is a central problem of net theory. This problem is known to be decidable but the complexity is still unknown. Whereas the problem is EXPSPACE-hard, no elementary upper bounds complexity are known. In this paper we consider the reversible reachability problem. This problem consists to decide if two configurations are reachable one from each other, or equivalently if they are in the same strongly connected component of the reachability graph. We show that this problem is EXPSPACE-complete. As an application of the introduced materials we characterize the reversibility domains of a vector addition system.