## 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.