Characterization of Termination for Linear Loop Programs

TL;DR

This paper provides a complete characterization and verification method for the termination of linear homogeneous programs using linear algebra, ensuring soundness, completeness, and numerical stability.

Contribution

It introduces necessary and sufficient conditions for termination and a complete, algebraic method to verify termination of linear homogeneous programs.

Findings

Complete algebraic characterization of termination

Verification reduces to orthogonality checks in vector spaces

Method guarantees soundness, completeness, and stability

Abstract

We present necessary and sufficient conditions for the termination of linear homogeneous programs. We also develop a complete method to check termination for this class of programs. Our complete characterization of termination for such programs is based on linear algebraic methods. We reduce the verification of the termination problem to checking the orthogonality of a well determined vector space and a certain vector, both related to loops in the program. Moreover, we provide theoretical results and symbolic computational methods guaranteeing the soundness, completeness and numerical stability of the approach. Finally, we show that it is enough to interpret variable values over a specific countable number field, or even over its ring of integers, when one wants to check termination over the reals.