Language Inclusion for Boundedly-Ambiguous Vector Addition Systems is Decidable

TL;DR

This paper proves that language inclusion for boundedly-ambiguous Vector Addition Systems with States (VASS) is decidable, while language equivalence remains highly complex, with results applicable to broader infinite-state systems.

Contribution

It establishes decidability of language inclusion for k-ambiguous VASS and shows Ackermann-hardness of language equivalence for deterministic VASS, advancing understanding of these problems.

Findings

Language inclusion for k-ambiguous VASS is decidable and in Ackermann complexity.

Language equivalence for deterministic VASS is Ackermann-hard.

Techniques apply to broader classes of infinite-state systems.

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.