We consider the problem of deciding termination of single-path while loops with integer variables, affine updates, and affine guard conditions. The question is whether such a loop terminates on all integer initial values. This problem is known to be decidable for the subclass of loops whose update matrices are diagonalisable, but the general case has remained open since being conjectured decidable by Tiwari in 2004. In this paper we show decidability of determining termination for arbitrary update matrices, confirming Tiwari's conjecture. For the class of loops considered in this paper, the question of deciding termination on a specific initial value is a longstanding open problem in number theory. The key to our decision procedure is in showing how to circumvent the difficulties inherent in deciding termination on a fixed initial value.

翻译：我们考虑了在以整数变量、折叠式更新和折叠式保护条件环绕时决定终止单一路径的问题。 问题在于这种环绕是否在所有整数初始值上都终止。 这个问题对于更新矩阵可以对等化的环绕子类来说是可分解的, 但一般情况自2004年提瓦里预测可分解以来一直没有解决。 本文显示,确定任意更新矩阵终止的可变性, 证实了蒂瓦里的猜想。 对于本文所考虑的环绕类别, 决定特定初始值终止的问题在数字理论上是一个长期的开放问题。 我们决定程序的关键在于显示如何避免在确定固定初始值终止时所固有的困难。