eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-05
130:1
130:17
10.4230/LIPIcs.ICALP.2023.130
article
Positivity Problems for Reversible Linear Recurrence Sequences
Kenison, George
1
Nieuwveld, Joris
2
Ouaknine, Joël
2
Worrell, James
3
Institute of Logic and Computation, TU Wien, Austria
Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Department of Computer Science, University of Oxford, UK
It is a longstanding open problem whether there is an algorithm to decide the Positivity Problem for linear recurrence sequences (LRS) over the integers, namely whether given such a sequence, all its terms are non-negative. Decidability is known for LRS of order 5 or less, i.e., for those sequences in which every new term depends linearly on the previous five (or fewer) terms. For simple LRS (i.e., those sequences whose characteristic polynomials have no repeated roots), decidability of Positivity is known up to order 9.
In this paper, we focus on the important subclass of reversible LRS, i.e., those integer LRS ⟨u_n⟩_{n=0}^∞ whose bi-infinite completion ⟨u_n⟩_{n=-∞}^∞ also takes exclusively integer values; a typical example is the classical Fibonacci (bi-)sequence ⟨ … , 5, -3, 2, -1, 1, 0, 1, 1, 2, 3, 5, … ⟩. Our main results are that Positivity is decidable for reversible LRS of order 11 or less, and for simple reversible LRS of order 17 or less.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol261-icalp2023/LIPIcs.ICALP.2023.130/LIPIcs.ICALP.2023.130.pdf
The Positivity Problem
Linear Recurrence Sequences
Verification