Reachability in symmetric VASS
{\L}ukasz Kami\'nski, S{\l}awomir Lasota

TL;DR
This paper studies the reachability problem in symmetric vector addition systems with states (VASS), showing it can be solved in PSPACE for symmetric groups, contrasting with Ackermannian complexity in general VASS.
Contribution
It demonstrates that reachability in symmetric VASS is PSPACE-complete, providing complexity bounds for various group symmetries and their combinations.
Findings
Reachability in symmetric VASS is in PSPACE.
Complexity varies with group symmetry, from trivial to symmetric groups.
Combining trivial and symmetric groups affects problem complexity.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Stability and Control of Uncertain Systems · Control Systems and Identification
