On the Separability Problem of VASS Reachability Languages

TL;DR

This paper proves that the regular separability problem for VASS reachability languages is decidable and highly complex, introducing a new proof object called doubly-marked graph transition sequences to facilitate the decision process.

Contribution

It introduces doubly-marked graph transition sequences and a decomposition algorithm that ensures faithfulness, enabling regular separation of VASS reachability languages.

Findings

Decidability of the regular separability problem for VASS reachability languages.

The problem is $ extbf{F}_{oldsymbol{ extomega}}$-complete, indicating high complexity.

A new proof object and decomposition method that preserve key properties for separation.

Abstract

We show that the regular separability problem of VASS reachability languages is decidable and $\mathbf{F}_{\omega}$-complete. At the heart of our decision procedure are doubly-marked graph transition sequences, a new proof object that tracks a suitable product of the VASS we wish to separate. We give a decomposition algorithm for DMGTS that not only achieves perfectness as known from MGTS, but also a new property called faithfulness. Faithfulness allows us to construct, from a regular separator for the $\mathbb{Z}$-versions of the VASS, a regular separator for the $\mathbb{N}$-versions. Behind faithfulness is the insight that, for separability, it is sufficient to track the counters of one VASS modulo a large number that is determined by the decomposition.