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.
翻译：我们考虑以下问题：给定 $d\times d$ 的有理矩阵 $A_1, \ldots, A_k$ 和一个多面体锥体 $\mathcal{C} \subset \mathbb{R}^d$，判断是否存在一个非零向量，其在被 $A_1, \ldots, A_k$ 乘以后的轨道被包含在 $\mathcal{C}$ 中。这个问题可以被理解为验证多路径线性更新和线性守卫条件下的循环终止。我们表明，对于交换可逆矩阵 $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$ 的子模是否包含“正”元素。
相关内容
微信扫码咨询专知VIP会员