## Termination of affine loops over the integers

*Mehran Hosseini*,
*Joël
Ouaknine*, and *James Worrell*
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 single 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 single initial value.

*Proceedings of ICALP 19*, LIPIcs 132, 2019. 13 pages.

PDF
© 2019 Mehran Hosseini, Joël Ouaknine, and James Worrell.

Imprint / Data Protection