On the Decidability of Membership in Matrix-exponential Semigroups
On the Decidability of Membership in Matrix-exponential Semigroups
复制标题
矩阵指数半群隶属度的可判定性
作者：
Joël Ouaknine;Amaury Pouly;João Sousa;J. Worrell
我们考虑矩阵指数半群的隶属问题的可判定性：给定 k∈ N 和方阵 A1, … , Ak, C，所有维度相同且具有实代数项，判定 C 是否包含在由矩阵指数 exp (Ai t) 生成的半群中，其中 i∈ { 1,… ,k} 且 t ≥ 0。这个问题可以看作 Babai 等人和 Cai 等人的连续类比等人解决乘法矩阵方程的问题，并应用于线性混合自动机和切换系统的可达性分析。我们的主要结果是，半群成员资格问题一般来说是不可判定的，但如果我们假设 A1, … , Ak 可交换，则可以判定。可判定性证明是通过简化为具有超越常数的整数规划版本来实现的。我们使用代数数对数线性形式的贝克定理以及其他工具给出了后者的决策过程。不可判定性结果通过希尔伯特第十问题的约简来显示。
We consider the decidability of the membership problem for matrix-exponential semigroups: Given k∈ N and square matrices A1, … , Ak, C, all of the same dimension and with real algebraic entries, decide whether C is contained in the semigroup generated by the matrix exponentials exp (Ai t), where i∈ { 1,… ,k} and t ≥ 0. This problem can be seen as a continuous analog of Babai et al.’s and Cai et al.’s problem of solving multiplicative matrix equations and has applications to reachability analysis of linear hybrid automata and switching systems. Our main results are that the semigroup membership problem is undecidable in general, but decidable if we assume that A1, … , Ak commute. The decidability proof is by reduction to a version of integer programming that has transcendental constants. We give a decision procedure for the latter using Baker’s theorem on linear forms in logarithms of algebraic numbers, among other tools. The undecidability result is shown by reduction from Hilbert’s Tenth Problem.