Regular Separability in Büchi Vector Addition Systems

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 a succinct encoding. 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. For finite-word VASS coverability languages, regular separability is known to be equivalent to disjointness, a result that carries over to more general WSTS. We show that, for infinite words, the situation is different. There are disjoint Büchi VASS languages where separability fails. Moreover, there is a natural class of WSTS such that for their languages of infinite words, intersection is decidable, but regular separability is undecidable.

Authors

• Pascal Baumann

Keywords

No keywords are indexed for this paper.