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
|