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