Termination of Real Linear Loops
For researchers in program analysis and verification, this work clarifies the boundary of decidability for a fundamental problem, providing practical algorithms for almost all cases.
The paper addresses the decidability of universal termination for linear and affine loops over the reals, showing that while the problem is undecidable in general, there exist sound partial algorithms that halt on all robust instances, and the set of non-robust instances has measure zero.
We study the problem of deciding universal termination of linear and affine loops over the reals in the bit-model of real computation. We show that both problems are as close to decidable as one can expect them to be: there exist sound partial algorithms that halt on all problem instances whose answer is robust under all sufficiently small perturbations. We further show that in each case the set of non-robust problem instances has Lebesgue measure zero.