We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASSes) 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 VASSes, thus to get decidability we investigate restricted subclasses. On 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 Ackermann-hard already for deterministic VASSes. 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.
翻译:我们研究了具有状态(VASS)的向量加法系统的语言包含与语言等价问题,其接受条件由接受状态集(更一般地,由某些上闭条件)定义。一般而言,即使对于一维VASS,语言等价问题也是不可判定的,因此为了获得可判定性,我们考察了受限子类。一方面,我们证明了任意自然数k下,VASS在k-歧义VASS中的语言包含问题是可判定的,甚至属于阿克曼复杂度类。另一方面,我们证明了对于确定性VASS,语言等价问题已经是阿克曼难的。这两个结果意味着在多种可能的限制条件下,语言包含与等价问题具有阿克曼完备性。我们的部分技术也可更广泛地应用于无限状态系统,即某些良结构转移系统的子类。