Ultimate Positivity is decidable for simple linear recurrence sequences

Joël Ouaknine and James Worrell

We consider the decidability and complexity of the Ultimate Positivity Problem, which asks whether all but finitely many terms of a given rational linear recurrence sequence (LRS) are positive. Using lower bounds in Diophantine approximation concerning sums of S-units, we show that for simple LRS (those whose characteristic polynomial has no repeated roots) the Ultimate Positivity Problem is decidable in polynomial space. If we restrict to simple LRS of a fixed order then we obtain a polynomial-time decision procedure. As a complexity lower bound we show that Ultimate Positivity for simple LRS is at least as hard as the decision problem for the universal theory of the reals: a problem that is known to lie between coNP and PSPACE.

Proceedings of ICALP 14, LNCS 8573, 2014. 12 pages.
Best Paper Award.

PDF © 2014 Springer-Verlag.