Characterising Robust Instances of Ultimate Positivity for Linear Dynamical Systems

TL;DR

This paper characterizes robust instances of the Ultimate Positivity Problem in linear dynamical systems, showing these instances form semialgebraic sets and are decidable using the First Order Theory of the Reals.

Contribution

It introduces the concept of robustness in the Ultimate Positivity Problem and characterizes the sets of robust instances as semialgebraic, enabling decision procedures.

Findings

Robust instances form semialgebraic sets.

Ultimate Positivity problem is decidable for robust instances.

Characterization uses the First Order Theory of the Reals.

Abstract

Linear Dynamical Systems, both discrete and continuous, are invaluable mathematical models in a plethora of applications such the verification of probabilistic systems, model checking, computational biology, cyber-physical systems, and economics. We consider discrete Linear Recurrence Sequences and continuous C-finite functions, i.e. solutions to homogeneous Linear Differential Equations. The Ultimate Positivity Problem gives the recurrence relation and the initialisation as input and asks whether there is a step $n_0$ (resp. a time $t_0$) such that the Linear Recurrence Sequence $u[n] \ge 0$ for $n > n_0$ (resp. solution to homogeneous linear differential equation $u(t) \ge 0$ for $t > t_0$). There are intrinsic number-theoretic challenges to surmount in order to decide these problems, which crucially arise in engineering and the practical sciences. In these settings, the difficult corner cases are seldom relevant: tolerance to the inherent imprecision is especially critical. We thus characterise \textit{robust} instances of the Ultimate Positivity Problem, i.e.\ inputs for which the decision is locally constant. We describe the sets of Robust YES and Robust NO instances using the First Order Theory of the Reals. We show, via the admission of quantifier elimination by the First Order Theory of the Reals, that these sets are semialgebraic.