对称向量加法系统可达性问题的复杂度分析
Reachability in symmetric VASS
- 研究对称性约束下的向量加法系统可达性问题
- 对称群情形下可达性可在PSPACE内解决，与维度无关
- 适用于关注复杂度降低的逻辑与验证领域研究者
我们研究带有状态的对称向量加法系统（symmetric VASS）中的可达性问题，其中转移规则在坐标置换群作用下保持不变。极端情况之一是平凡群，对应一般VASS；另一极端是完全对称群，我们证明此时可达性问题可在PSPACE内解决，且不依赖输入VASS的维度（与一般VASS的阿克曼级复杂度形成对比）。我们还考察了交错群和循环群等其他群结构。此外，为应对数据VASS中可达性问题尚未解决的现状，我们评估了当群由平凡群与对称群组合而成时，复杂度的下降程度。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。