Robust Positivity Problems for Linear Recurrence Sequences

TL;DR

This paper investigates the decidability of robust positivity problems for linear recurrence sequences, accounting for initial perturbations, and establishes sharp decidability results that delineate the limits of current techniques.

Contribution

It introduces decision procedures for robust positivity problems with explicit initial perturbations and proves their sharp decidability boundaries, highlighting the complexity of the problem.

Findings

Decidability results for robust positivity with initial perturbations

Sharp boundaries established for the limits of current techniques

Implications for number-theoretic decision problems

Abstract

Linear Recurrence Sequences (LRS) are a fundamental mathematical primitive for a plethora of applications such as the verification of probabilistic systems, model checking, computational biology, and economics. Positivity (are all terms of the given LRS non-negative?) and Ultimate Positivity (are all but finitely many terms of the given LRS non-negative?) are important open number-theoretic decision problems. Recently, the robust versions of these problems, that ask whether the LRS is (Ultimately) Positive despite small perturbations to its initialisation, have gained attention as a means to model the imprecision that arises in practical settings. However, the state of the art is ill-equipped to reason about imprecision when its extent is explicitly specified. In this paper, we consider Robust Positivity and Ultimate Positivity problems where the neighbourhood of the initialisation, expressed in a natural and general format, is also part of the input. We contribute by proving sharp decidability results: decision procedures at orders our techniques are unable to handle for general LRS would entail significant number-theoretic breakthroughs.