Affine Extensions of Integer Vector Addition Systems with States

Affine Extensions of Integer Vector Addition Systems with States
复制标题

整数向量加法系统的仿射扩展

DOI：
10.46298/lmcs-17(3:1)2021
复制
发表时间：
2019
期刊：
ArXiv
影响因子：
--
通讯作者：
Filip Mazowiecki
Filip Mazowiecki
中科院分区：
--
文献类型：
--
作者：
Michael Blondin;C. Haase;Filip Mazowiecki

文献摘要

被引文献

相似文献

我们研究了仿射$\mathbb{Z}$-Vass的可达性问题 状态转移执行仿射的整数向量加法系统 柜台上的变形。这个问题很容易被认为是无法决定的 一般而言，我们将自己限制为仿射$\mathbb{Z}$-vass 具有有限么半群性质(AFMP-$\mathbb{Z}$-vass)。后者拥有 由出现在其仿射中的矩阵生成的么半群的性质 变换是有限的。AFMP-$\mathbb{Z}$-VASS类包含 计数器机器的经典操作，例如重置，排列， 转移和复制。我们证明了AFMP-$\mathbb{Z}$-VASS的可达性 降低到控制状态增长的$\mathbb{Z}$-Vass中的可达性 矩阵么半群的大小是线性的。我们的建设表明， AFMP-$\mathbb{Z}$-VASS的可达性关系是半线性的，并且在 特殊使我们能够展示在$\mathbb{Z}$-VASS中的可达性 传输和$\mathbb{Z}$-带副本的VASS为PSPACE-Complete。然后我们专注于 关于单生仿射$\mathbb{Z}$-Vass的可达性问题 么半群：(可能是无限的)由单个矩阵生成的矩阵么半群。我们 证明在特定情况下，可达性问题是可以决定的 类，反驳了关于无限仿射$\mathbb{Z}$-vass的一个猜想 我们在本文的初步版本中提出的矩阵么半群。我们互为补充 通过给出一个具有单因矩阵的仿射$\mathbb{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.