Termination of linear loops under commutative updates

Abstract

We consider the following problem: given $d\times d$ rational matrices $A_1,\dots ,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,\dots ,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,\dots ,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,\dots ,X_k]$ as well as the polynomial semiring ${\mathbb{R}}_{\ge 0}[X_1,\dots ,X_k]$. The loop termination problem is then reduced to deciding whether a submodule of ${\left(\mathbb{R}[X_1,\dots ,X_k]\right)}^n$ contains a ``positive'' element.

6 pages