Separability of Reachability Sets of Vector Addition Systems

TL;DR

This paper investigates the decidability of separability problems for reachability sets of Vector Addition Systems, showing that certain classes of sets can be separated using modular and unary sets.

Contribution

It proves the decidability of modular and unary separability for reachability sets in Vector Addition Systems and related models, advancing understanding of their structural properties.

Findings

Decidability of modular separability for reachability sets.

Decidability of unary separability for reachability sets.

Applicable to Petri Nets and Vector Addition Systems.

Abstract

Given two families of sets $\mathcal{F}$ and $\mathcal{G}$, the $\mathcal{F}$ separability problem for $\mathcal{G}$ asks whether for two given sets $U, V \in \mathcal{G}$ there exists a set $S \in \mathcal{F}$, such that $U$ is included in $S$ and $V$ is disjoint with $S$. We consider two families of sets $\mathcal{F}$: modular sets $S \subseteq \mathbb{N}^d$, defined as unions of equivalence classes modulo some natural number $n \in \mathbb{N}$, and unary sets. Our main result is decidability of modular and unary separability for the class $\mathcal{G}$ of reachability sets of Vector Addition Systems, Petri Nets, Vector Addition Systems with States, and for sections thereof.