Termination of linear loops under commutative updates

TL;DR

This paper proves the decidability of loop termination for linear loops with commutative, invertible matrices by translating the problem into algebraic module theory over polynomial rings.

Contribution

It introduces an algebraic approach connecting loop termination with modules over polynomial rings, enabling decidability results for a class of linear loops.

Findings

Decidability established for commuting invertible matrices.

Connection made between loop termination and modules over polynomial rings.

Reduction of the problem to algebraic module containment questions.

Abstract

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.