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.
翻译:带状态向量加法系统(VASS)是并发理论中的经典模型。语法向量加法系统(GVAS),即下推VASS,通过使用上下文无关文法控制加法操作对VASS进行了扩展。本文主要研究一维薄GVAS(thin 1-GVAS)的可达性问题,这是一个结构受限但仍具表达力的子类。通过采用索引度量复杂度指标,并将VASS可达性研究中发展的分解技术推广至GVAS的文法生成推导树,我们为一维薄GVAS建立了有效的整数规划系统。由此,针对索引为$k$的薄1-GVAS可达性问题,我们得到了具有$\mathbf{F}_{2k}$复杂度的非确定性算法,该结果给出了比先前更紧的上界。