Termination of linear loops under commutative updates

02/02/2023

∙

by   Ruiwen Dong, et al.

∙

0

∙

share

We consider the following problem: given d × d rational matrices A_1, …, A_k and a polyhedral cone 𝒞⊂ℝ^d, decide whether there exists a non-zero vector whose orbit under multiplication by A_1, …, A_k is contained in 𝒞. 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, …, 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 ℝ[X_1, …, X_k] as well as the polynomial semiring ℝ_≥ 0[X_1, …, X_k]. The loop termination problem is then reduced to deciding whether a submodule of (ℝ[X_1, …, X_k])^n contains a “positive” element.