On Selective Unboundedness of VASS

TL;DR

This paper extends techniques for checking various unboundedness properties in vector addition systems with states, providing new exponential and polynomial space bounds for several problems including reversal-boundedness and regularity detection.

Contribution

It introduces generalized unboundedness properties and extends Rackoff's technique to establish optimal exponential and polynomial space bounds.

Findings

New exponential space bounds for reversal-boundedness detection

Optimal bounds for place-boundedness and regularity detection

Polynomial-space bounds when the dimension is fixed

Abstract

Numerous properties of vector addition systems with states amount to checking the (un)boundedness of some selective feature (e.g., number of reversals, run length). Some of these features can be checked in exponential space by using Rackoff's proof or its variants, combined with Savitch's theorem. However, the question is still open for many others, e.g., reversal-boundedness. In the paper, we introduce the class of generalized unboundedness properties that can be verified in exponential space by extending Rackoff's technique, sometimes in an unorthodox way. We obtain new optimal upper bounds, for example for place-boundedness problem, reversal-boundedness detection (several variants exist), strong promptness detection problem and regularity detection. Our analysis is sufficiently refined so as we also obtain a polynomial-space bound when the dimension is fixed.