Regular Separability in B\"{u}chi VASS

TL;DR

This paper investigates the regular separability problem for B"uchi VASS languages, establishing decidability and complexity results, and introduces methods to characterize and verify inseparability witnesses.

Contribution

It provides the first decidability results for regular separability in B"uchi VASS and introduces a symbolic approach to identify inseparability witnesses.

Findings

Decidable in general for B"uchi VASS languages.

PSPACE-complete in 1-dimensional case with succinct updates.

Characterization and symbolic representation of inseparability witnesses.

Abstract

We study the ($\omega$-)regular separability problem for B\"uchi VASS languages: Given two B\"uchi 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.