aiqbench analysis
This paper advances theoretical computer science by proving that the reachability problem in symmetric Vector Addition Systems with States (VASS) is solvable in PSPACE, a significant reduction from the Ackermannian complexity of general VASS. The work provides crucial complexity bounds for systems where transition rules are invariant under specific permutation groups, offering new insights into the structural constraints that make verification tractable.
Reachability in Symmetric VASS
arXiv:2506.23578v3 Announce Type: replace-cross 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.
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.
Formal Languages and Automata Theory (cs.FL); Computation and Language (cs.CL)
arXiv:2506.23578 [cs.FL]
(or arXiv:2506.23578v3 [cs.FL] for this version)
https://doi.org/10.48550/arXiv.2506.23578 Focus to learn more arXiv-issued DOI via DataCite
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 209 words
Related coverage
Reachability in 3-VAS
arXiv · Aug 6, 2026
Categorical Approach to Conflict Resolution:A Corrected Correspondence between Category Theory and the Graph Model for Conflict Resolution
arXiv · Sep 29, 2026
Tilt as a Certified Resource: Preserving Motor Wrench-Rate Authority on Articulated Multirotors
arXiv · Sep 21, 2026
An Enclosed Mode Is a Gauge Choice: Topology Relative to Reach in Certified Code World Models
arXiv · Sep 1, 2026