Termination of linear loops under commutative updates
We consider the following problem: given d × d rational matrices A1, …, Ak and a polyhedral cone , decide whether there exists a non-zero vector whose orbit under multiplication by A1, …, Ak is contained in . This problem can be interpreted as verifying the termination of multi-path while loops with...
| Main Author: | |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Association for Computing Machinery
2023
|
| Summary: | We consider the following problem: given d × d rational matrices A1, …, Ak and a polyhedral cone , decide whether there exists a non-zero vector whose orbit under multiplication by A1, …, Ak 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 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 as well as the polynomial semiring . The loop termination problem is then reduced to deciding whether a submodule of contains a “positive” element. |
|---|