Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Chengfeng Xue, Yuxi Fu

TL;DR

This paper tackles the reachability problem for one-dimensional thin grammar vector addition systems (1-GVAS). It extends the KLM decomposition from VASS to grammar-controlled runs by introducing KLM trees and a ranking-based refinement process, then specializes to the 1-D case to obtain a nondeterministic algorithm with a complexity bound in the fast-growing class $F_{2k}$ for a $k$-indexed 1-GVAS. The core advance is a generalization of the KLM framework to tree-structured derivations via a characteristic ILP system and a sequence of refinements culminating in perfect KLM trees, which act as certificates for reachability. The result significantly tightens prior bounds (from $F_{6k-4}$ to $F_{2k}$) and provides a structured, certificate-based approach that can be leveraged for decision procedures and complexity analyses in related grammar-controlled VASS models.

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.

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

TL;DR

This paper tackles the reachability problem for one-dimensional thin grammar vector addition systems (1-GVAS). It extends the KLM decomposition from VASS to grammar-controlled runs by introducing KLM trees and a ranking-based refinement process, then specializes to the 1-D case to obtain a nondeterministic algorithm with a complexity bound in the fast-growing class for a -indexed 1-GVAS. The core advance is a generalization of the KLM framework to tree-structured derivations via a characteristic ILP system and a sequence of refinements culminating in perfect KLM trees, which act as certificates for reachability. The result significantly tightens prior bounds (from to ) and provides a structured, certificate-based approach that can be leveraged for decision procedures and complexity analyses in related grammar-controlled VASS models.

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 complexity is obtained for the reachability of thin 1-GVAS with index , yielding a tighter upper bound than the previous one.
Paper Structure (28 sections, 33 theorems, 33 equations, 5 figures, 1 table, 1 algorithm)

This paper contains 28 sections, 33 theorems, 33 equations, 5 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Grammar Vector Addition Systems
  4. Thinness and Index
  5. Derivation Trees
  6. Related Problems
  7. KLM Trees
  8. Divisions
  9. KLM Components and KLM Trees
  10. The Characteristic System
  11. Ranks
  12. Solutions and Boundedness
  13. Decomposing KLM Trees
  14. Perfectness
  15. Configuration Constraining
  16. ...and 13 more sections

Key Result

theorem 1

The reachability problem for thin 1-GVAS indexed by $k$ is in $\mathbf{F}_{2k}$.

Figures (5)

  • Figure 1: The production graph and the index.
  • Figure 2: Configurations (terminal configurations omitted).
  • Figure 3: A strongly-connected segment captured by a KLM component.
  • Figure 4: The refinement sequence.
  • Figure 5: The division of bounded segments.

Theorems & Definitions (50)

  • theorem 1
  • lemma 1: Bad sequences
  • lemma 2: Pottier
  • definition 1: Thinness
  • definition 2: Index
  • definition 3
  • lemma 3
  • definition 4
  • definition 5
  • definition 6
  • ...and 40 more