Exploring VASS Parameterised by Geometric Dimension

TL;DR

This paper investigates the geometric dimension of VASS, showing it as a potentially more effective parameter for analyzing reachability, coverability, and boundedness problems, leading to improved complexity bounds.

Contribution

It introduces the systematic study of geometric dimension in VASS and improves classical results by replacing the standard dimension with geometric dimension in key problems.

Findings

Coverability runs are bounded by n^{2^{O(g)}}

Unboundedness runs are bounded by n^{2^{O(g log g)}}

Geometric dimension offers tighter complexity bounds than standard dimension

Abstract

The geometric dimension $g$ of a Vector Addition System with States (VASS) is the dimension of the vector space generated by cycles in the VASS; this parameter refines the standard dimension $d$, the number of counters. Recently, it was discovered that the fastest-known algorithm for solving the reachability problem for VASS has the same complexity in terms of $g$ as in terms of $d$. This suggests that the geometric dimension may in fact be a more adequate parameter for measuring the complexity of VASS reachability problems. We initiate a more systematic study of the geometric dimension. We discuss differences between two parameters: the geometric dimension and the SCC dimension. Our main technical result states that classical results about the coverability and boundedness problems can be improved from dimension $d$ to geometric dimension $g$. Namely, coverability is witnessed by runs of length $n^{2^{\mathcal{O}(g)}}$ instead of $n^{2^{\mathcal{O}(d)}}$, and unboundedness can be witnessed by runs of length $n^{2^{\mathcal{O}(g\log g)}}$ instead of $n^{2^{\mathcal{O}(d\log d )}}$, where $n$ is the size of the instance. We also study integer reachability and simultaneous unboundedness in VASS parameterised by the geometric dimension.