Reachability in symmetric VASS

TL;DR

This paper investigates reachability in symmetric VASS and shows that symmetry can drastically alter complexity. It proves PSPACE-completeness for the full symmetric group $S_d$ (and the alternating group $A_d$) regardless of dimension, while establishing PSPACE-hardness for other groups, and provides upper/lower bounds for wreath-product combinations. It extends techniques to data-VASS and identifies a decidable subclass $(S_∞ wr I_n)$-VASS, indicating a potential group-based taxonomy of reachability complexity in VASS and outlining open questions for a complete classification.

Abstract

We investigate the reachability problem in symmetric vector addition systems with states (VASS), where transitions are invariant under a group of permutations of coordinates. One extremal case, the trivial groups, yields general VASS. In another extremal case, the symmetric groups, we show that the reachability problem can be solved in PSPACE, regardless of the dimension of input VASS (to be contrasted with Ackermannian complexity in general VASS). We also consider other groups, in particular alternating and cyclic ones. Furthermore, motivated by the open status of the reachability problem in data VASS, we estimate the gain in complexity when the group arises as a combination of the trivial and symmetric groups.

Figures (3)

• Figure 1: A sequential vass.
• Figure 2: A 2-dimensional data vass as a $(I_{2} \wr S_{\infty})$- vass. States are $Q = \left\{p, q, r\right\}$, and transitions are given by orbit representatives. The data values $a\neq b\in \mathbb{N}$ are chosen arbitrarily.
• Figure :

Theorems & Definitions (31)

• Lemma 1
• proof : Proof of Lemma \ref{['lem:zrun']}
• Theorem 2: IntCaratheodory, Thm. 1(ii)
• Lemma 3
• proof
• Remark 4
• Remark 5
• Lemma 6
• proof
• Lemma 7