Termination of Real Linear Loops

TL;DR

This paper investigates the decidability of universal termination for linear and affine loops over reals, demonstrating that robust instances are semi-decidable and non-robust cases are measure-zero.

Contribution

It establishes that robust termination problems are semi-decidable and that non-robust instances are negligible in measure, advancing understanding of real loop termination.

Findings

Robust instances are semi-decidable.

Non-robust instances have Lebesgue measure zero.

Decidability is as close to possible given the problem's nature.

Abstract

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.