Language Inclusion for Boundedly-Ambiguous Vector Addition Systems is Decidable
Wojciech Czerwiński, Piotr Hofman
TL;DR
This work investigates language inclusion and equivalence for VASS under acceptance by states, identifying undecidability in general and proving decidability results for restricted subclasses. The authors introduce a suite of techniques, including regular lookahead decorations and complement constructions, to show that inclusion is Ackermann-decidable for k-ambiguous VASS and that language equivalence is Ackermann-hard for deterministic VASS, with unambiguous and boundedly-ambiguous cases treated via reductions to deterministic HVASS. The results yield Ackermann-completeness for language inclusion and equivalence in several restricted settings and suggest broader applicability to well-structured transition systems. The study advances understanding of tractable boundaries in infinite-state formalisms and lays groundwork for extensions to other models and separability frameworks.
Abstract
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.