一句话：证明有界歧义 VASS 的语言包含可判定，并确立若干限制下等价问题的 Ackermann 完全性。
本文研究带状态向量加法系统（VASS）的语言包含与语言等价问题，接受条件由接受状态集合（更一般地，由向上封闭条件）给出。一般情形下，即使一维 VASS 的语言等价也不可判定，因此作者转向受限子类。核心上界结果是：任意自然数 k 下，VASS 语言包含于 k-歧义 VASS 是可判定的，且属于 Ackermann 复杂度。下界方面，确定性 VASS 的语言等价已是 Ackermann 困难。两者结合推出若干限制下语言包含与语言等价的 Ackermann 完全性。作者的方法还可推广到更广的无限状态系统，特别是某类良结构迁移系统。
We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASS) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general, the problem of language equivalence is undecidable even for one-dimensional VASS, thus to get decidability we investigate restricted subclasses. On the one hand, we show that the problem of language inclusion of a VASS in k-ambiguous VASS (for any natural k) is decidable and even in Ackermann. On the other hand, we prove that the language equivalence problem is already Ackermann-hard for deterministic VASS. These two results imply Ackermann-completeness for language inclusion and equivalence in several possible restrictions. Some of our techniques can be also applied in much broader generality in infinite-state systems, namely for some subclass of well-structured transition systems.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CzerwinskiH22,
title = {Language Inclusion for Boundedly-Ambiguous Vector Addition Systems is Decidable},
author = {Wojciech Czerwiński and Piotr Hofman},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:27)2025}
}