2023/02/02 by Ruiwen Dong, Dong, Ruiwen
Computer Science · Engineering · Mathematics · #Advanced Differential Equations and Dynamical Systems #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO) #Polynomial and algebraic computation #Rings and Algebras (math.RA) #graph theory and CDMA systems
paper · pdf · doi:10.48550/arxiv.2302.01003
openalex publication_date 2023/02/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We consider the following problem: given d × d rational matrices A1, …, Ak and a polyhedral cone C ⊂ ℝd, decide whether there exists a non-zero vector whose orbit under multiplication by A1, …, Ak is contained in 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 A1, …, Ak. 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 ℝ[X1, …, Xk] as well as the polynomial semiring ℝ≥ 0[X1, …, Xk]. The loop termination problem is then reduced to deciding whether a submodule of (ℝ[X1, …, Xk])n contains a ``positive'' element.