On the termination of integer loops

Abstract

In this paper we study the decidability of termination of several variants of simple integer loops, without branching in the loop body and with affine constraints as the loop guard (and possibly a precondition). We show that termination of such loops is undecidable in some cases, in particular, when the body of the loop is expressed by a set of linear inequalities where the coefficients are from ℤ∪{r} with r an arbitrary irrational; or when the loop is a sequence of instructions, that compute either linear expressions or the step function. The undecidability result is proven by a reduction from counter programs, whose termination is known to be undecidable. For the common case of integer constraints loops with rational coefficients only we have not succeeded in proving decidability nor undecidability of termination, however, this attempt led to the result that a Petri net can be simulated with such a loop, which implies some interesting lower bounds. For example, termination for a given input is at least EXPSPACE-hard. © 2012 Springer-Verlag.