An Approach to Regular Separability in Vector Addition Systems

TL;DR

This paper introduces a general method for deciding regular separability of vector addition system languages, extending previous results to broader classes and addressing an open problem in formal language theory.

Contribution

It proposes a unified approach to regular separability in VASS, covering multiple subclasses and generalizing prior decidability results.

Findings

Decidable regular separability for one-dimensional VASS

Decidable regular separability for VASS coverability languages

Decidable regular separability for integer VASS languages

Abstract

We study the problem of regular separability of languages of vector addition systems with states (VASS). It asks whether for two given VASS languages K and L, there exists a regular language R that includes K and is disjoint from L. While decidability of the problem in full generality remains an open question, there are several subclasses for which decidability has been shown: It is decidable for (i) one-dimensional VASS, (ii) VASS coverability languages, (iii) languages of integer VASS, and (iv) commutative VASS languages. We propose a general approach to deciding regular separability. We use it to decide regular separability of an arbitrary VASS language from any language in the classes (i), (ii), and (iii). This generalizes all previous results, including (iv).