paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Affine Extensions of Integer Vector Addition Systems with States

带状态整数向量加法系统的仿射扩展
LMCS vol.Volume 17, Issue 32021匹配度 1/10 · 该论文研究仿射 Z-VASS 的可达性等逻辑与自动机理论问题,属于纯形式化验证/自动机理论,与用户关注的 LLM/Agent 结合静态分析、浮点程序分析、贝叶斯程序分析等方向均无明显交叉。引用 12 inbox
Michael Blondin, Christoph Haase, Filip Mazowiecki, Mikhail Raskin
crossref: 2026-09-10

AI 速览

一句话:研究仿射 Z-VASS 可达性,将有限矩阵幺半群情形归约到 Z-VASS,证明转移/复制变体 PSPACE 完全,并讨论单基因矩阵。

本文研究带状态整数向量加法系统(Z-VASS)的仿射扩展,一般可达性不可判定。作者引入有限矩阵幺半群性质的 afmp-Z-VASS,该类比重置、置换、转移和复制更强。方法是将 afmp-Z-VASS 可达性归约到普通 Z-VASS,控制状态数随矩阵幺半群大小线性增长,由此证明可达关系半线性,并得到带转移与带复制 Z-VASS 可达性为 PSPACE 完全。最后研究单基因矩阵幺半群的仿射 Z-VASS,证明一个特定子类可判定,否证了此前关于无限矩阵幺半群的猜想,并给出一个单基因矩阵幺半群但可达关系不可判定的反例。

问题
仿射 Z-VASS 的可达性问题:转移对整数计数器施加仿射变换,一般情形不可判定;论文旨在刻画可判定片段及其复杂度。
方法
引入有限矩阵幺半群性质的 afmp-Z-VASS,将可达性归约到普通 Z-VASS,并研究单基因矩阵幺半群的仿射系统。
评估
通过归约证明 afmp-Z-VASS 可达关系半线性,导出带转移/复制 Z-VASS 的 PSPACE 完全性;给出单基因矩阵幺半群下可判定与不可判定的具体结果。
原文摘要(Abstract)

We study the reachability problem for affine $\mathbb{Z}$-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine $\mathbb{Z}$-VASS with the finite-monoid property (afmp-$\mathbb{Z}$-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-$\mathbb{Z}$-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-$\mathbb{Z}$-VASS reduces to reachability in a $\mathbb{Z}$-VASS whose control-states grow linearly in the size of the matrix monoid. Our construction shows that reachability relations of afmp-$\mathbb{Z}$-VASS are semilinear, and in particular enables us to show that reachability in $\mathbb{Z}$-VASS with transfers and $\mathbb{Z}$-VASS with copies is PSPACE-complete. We then focus on the reachability problem for affine $\mathbb{Z}$-VASS with monogenic monoids: (possibly infinite) matrix monoids generated by a single matrix. We show that, in a particular case, the reachability problem is decidable for this class, disproving a conjecture about affine $\mathbb{Z}$-VASS with infinite matrix monoids we raised in a preliminary version of this paper. We complement this result by presenting an affine $\mathbb{Z}$-VASS with monogenic matrix monoid and undecidable reachability relation.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1300,
  title = {Affine Extensions of Integer Vector Addition Systems with States},
  author = {Michael Blondin and Christoph Haase and Filip Mazowiecki and Mikhail Raskin},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 17, Issue 3},
  year = {2021},
  doi = {10.46298/lmcs-17(3:1)2021}
}