Reachability in symmetric VASS
This addresses a theoretical complexity problem in formal verification and automata theory, with potential applications in systems modeling, but is incremental as it builds on known VASS frameworks.
The paper tackles the reachability problem in symmetric vector addition systems with states (VASS), showing that for symmetric groups, reachability can be solved in PSPACE regardless of dimension, contrasting with Ackermannian complexity in general VASS.
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.