Termination of Triangular Integer Loops is Decidable

TL;DR

This paper proves that it is decidable whether certain affine integer loops with triangular update matrices terminate, advancing understanding of loop termination in program analysis.

Contribution

It establishes the decidability of termination for affine integer loops with triangular update matrices, a previously unresolved case.

Findings

Decidability of termination for triangular affine integer loops

Extension of known decidability results to a broader class of loops

Provides a basis for automated termination analysis in this class

Abstract

We consider the problem whether termination of affine integer loops is decidable. Since Tiwari conjectured decidability in 2004, only special cases have been solved. We complement this work by proving decidability for the case that the update matrix is triangular.