Termination of Triangular Integer Loops is Decidable

Abstract

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