In this talk, I will present our recent study on 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 Z U {r} with r an arbitrary irrational; when the loop is a sequence of instructions, that compute either linear expressions or the step function; or when the loop body is a piecewise linear deterministic update with two pieces. The undecidability result is proven by a reduction from counter programs, whose termination is known to be undecidable. For the common case of integer constraint 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 (partial) input is at least EXPSPACE-hard.

Joint work with Amir M. Ben-Amram (The Tel-Aviv Academic College) and Samir Genaim (Complutense University of Madrid ).