arXiv · 2301.11242
Regular Separability in Büchi VASS
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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Pascal Baumann, Roland Meyer, Georg Zetzsche. 2023-01-26. Regular Separability in Büchi VASS. https://arxiv.org/abs/2301.11242
Cite the original work for its findings. Save a collection to share your selection of sources.