Characterising Robust Instances of Ultimate Positivity for Linear Dynamical Systems

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.