Positivity of Nearly Linearly Recurrent Sequences

TL;DR

This paper introduces a decision procedure for determining positivity in nearly linear recurrent sequences of order two, extending previous work on linear recurrences and connecting to control theory and program analysis.

Contribution

It presents the first decision procedure for the Positivity Problem in nearly linear recurrences of order two, utilizing a novel transcendence result for infinite series.

Findings

Decides positivity for nearly linear recurrences of order two.

Establishes a new transcendence result for infinite series.

Links the problem to control theory and program analysis.

Abstract

Nearly linear recurrences are a generalisation of linear recurrences and are instances of linear time-invariant systems in control theory and linear constraint loops in program analysis. In this paper we formulate the Positivity Problem for such recurrences. This asks whether all sequences satisfying a given recurrence with given initial conditions are positive. This problem is a generalisation of the Positivity Problem for linear recurrence sequences, and is a special case of the non-reachability problem for linear time-invariant systems. Our main contribution is a decision procedure for the Positivity Problem for recurrences of order two. The termination proof of our procedure relies on a new transcendence result for infinite series that is of independent interest.