交换更新下线性循环的终止性
Termination of linear loops under commutative updates
AI总结：
本文研究交换可逆矩阵更新下多路径线性循环的终止性判定问题，通过将其转化为多项式环与多项式半环上模中是否存在正元素的代数问题，证明了该问题是可判定的。
摘要：
我们考虑如下问题：给定 $d \times d$ 有理矩阵 $A_1, \ldots, A_k$ 和一个多面体锥 $\mathcal{C} \subset \mathbb{R}^d$，判定是否存在一个非零向量，其在 $A_1, \ldots, A_k$ 乘法作用下的轨道包含在 $\mathcal{C}$ 中。该问题可以解释为验证具有线性更新和线性守卫条件的多路径 while 循环的终止性。我们证明，对于可交换的可逆矩阵 $A_1, \ldots, A_k$，该问题是可判定的。我们的判定过程的关键在于以纯代数的方式重新解释这一问题。具体而言，我们发现它与多项式环 $\mathbb{R}[X_1, \ldots, X_k]$ 以及多项式半环 $\mathbb{R}_{\geq 0}[X_1, \ldots, X_k]$ 上的模之间的联系。循环终止问题随之被归约为判定 $\left(\mathbb{R}[X_1, \ldots, X_k]\right)^n$ 的一个子模是否包含一个“正”元素。
英文摘要：
We consider the following problem: given $d \times d$ rational matrices $A_1, \ldots, A_k$ and a polyhedral cone $\mathcal{C} \subset \mathbb{R}^d$, decide whether there exists a non-zero vector whose orbit under multiplication by $A_1, \ldots, A_k$ is contained in $\mathcal{C}$. This problem can be interpreted as verifying the termination of multi-path while loops with linear updates and linear guard conditions. We show that this problem is decidable for commuting invertible matrices $A_1, \ldots, A_k$. The key to our decision procedure is to reinterpret this problem in a purely algebraic manner. Namely, we discover its connection with modules over the polynomial ring $\mathbb{R}[X_1, \ldots, X_k]$ as well as the polynomial semiring $\mathbb{R}_{\geq 0}[X_1, \ldots, X_k]$. The loop termination problem is then reduced to deciding whether a submodule of $\left(\mathbb{R}[X_1, \ldots, X_k]\right)^n$ contains a ``positive'' element.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
