On the Reachability Problem for One-Dimensional Thin Grammar Vector Addition Systems

TL;DR

This paper investigates the reachability problem in a restricted subclass of grammar-controlled vector addition systems, introducing a new algorithm with improved complexity bounds for one-dimensional cases.

Contribution

It extends the decomposition technique to grammar-based systems and establishes an effective integer programming approach for thin 1-GVAS, improving complexity bounds.

Findings

Developed a nondeterministic algorithm with $ extbf{F}_{2k}$ complexity for thin 1-GVAS reachability.

Generalized decomposition techniques from VASS to grammar-generated derivation trees.

Provided tighter upper bounds for the reachability problem in thin 1-GVAS.

Abstract

Vector addition systems with states (VASS) are a classic model in concurrency theory. Grammar vector addition systems (GVAS), equivalently, pushdown VASS, extend VASS by using a context-free grammar to control addition. In this paper, our main focus is on the reachability problem for one-dimensional thin GVAS (thin 1-GVAS), a structurally restricted yet expressive subclass. By adopting the index measure for complexity, and by generalizing the decomposition technique developed in the study of VASS reachability to grammar-generated derivation trees of GVAS, an effective integer programming system is established for a thin 1-GVAS. In this way, a nondeterministic algorithm with $\mathbf{F}_{2k}$ complexity is obtained for the reachability of thin 1-GVAS with index $k$, yielding a tighter upper bound than the previous one.