Towards termination analysis and ranking function synthesis for non-linear constraint loops

Consider a loop of the form "while x in C do x := f(x);" where C, the so-called guard, is a subset of some finite-dimensional euclidean space and f is a function, called the update.

Termination analysis for loops of this kind is a central problem in automated verification. Beyond establishing termination, one is often interested in the existence of a so-called ranking function, i.e., a real-valued function g satisfying g(x) > g(f(x)) + 1 for all x in C.

While the general problem of deciding termination of such loops is known to be undecidable, a classical result due to Tiwari (2004) asserts decidability of termination in the case where the guard is a polyhedron and the update is an affine map. In this case, the problem of deciding the existence of a linear ranking function can be reduced to linear programming in polynomial time. The existence of a ranking function is sufficient but not necessary for the termination of the program.

In this talk I will report on ongoing work to extend these results to the non-linear case. I will show that a loop with a continuous update and compact semi-algebraic guard has a polynomial ranking function if and only if it terminates and that termination is decidable if the guard is compact semi-algebraic and the update is an affine map.

This is joint work with Joël Ouaknine and James Worrell.