Regular Separability in Büchi VASS

Pascal Baumann; Roland Meyer; Georg Zetzsche

paper

Regular Separability in Büchi VASS

arXiv:2301.11242

Abstract

We study the ( $ω$ -)regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages $L_{1}$ and $L_{2}$ , check whether there is a regular language that fully contains $L_{1}$ while remaining disjoint from $L_{2}$ . We show that the problem is decidable in general and PSPACE-complete in the 1-dimensional case, assuming succinct counter updates. The results rely on several arguments. We characterize the set of all regular languages disjoint from $L_{2}$ . Based on this, we derive a (sound and complete) notion of inseparability witnesses, non-regular subsets of $L_{1}$ . Finally, we show how to symbolically represent inseparability witnesses and how to check their existence.