On linear recurrence sequences and loop termination (a survey)

Joël Ouaknine and James Worrell

A sequence of real numbers is said to be positive if all terms are positive, and ultimately positive if all but finitely many terms are positive. In this article we survey recent progress on long-standing open problems concerning deciding the positivity and ultimate positivity of integer linear recurrence sequences. We briefly discuss some of the many contexts in which these problems arise, and relate them to the well-known Skolem Problem, which asks whether a given linear recurrence sequence has a zero term. We also highlight some of the mathematical techniques that have been used to obtain decision procedures for these problems, pointing out obstacles to further progress.

In the second half of this survey we move on to closely related questions concerning the termination of linear while loops. This is a well-studied subject in software verification and by now there is rich toolkit of techniques to prove termination in practice. However the decidability of termination for some of the most basic types of loop remains open. Here again we discuss recent progress and remaining open problems.

ACM SIGLOG News 2(2), 2015. 9 pages.

PDF © 2015 Joël Ouaknine and James Worrell.