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.

翻译：线性动力系统（包括离散与连续形式）在众多应用中具有不可估量的数学建模价值，例如概率系统验证、模型检测、计算生物学、信息物理系统以及经济学等领域。本文考虑离散线性递推序列与连续C有限函数（即齐次线性微分方程的解）。最终正性问题以递推关系与初始条件为输入，询问是否存在步数$n_0$（或时间$t_0$），使得线性递推序列$u[n] \ge 0$对所有$n > n_0$成立（或齐次线性微分方程的解$u(t) \ge 0$对所有$t > t_0$成立）。解决这些问题需要克服内在的数论挑战，而这些问题在工程与实践科学中至关重要。在此类场景中，困难的边界情形鲜有实际意义：对固有非精确性的容错能力尤为关键。因此，我们刻画了最终正性问题的\textit{鲁棒}实例，即决策结果在局部保持恒定的输入。利用实数一阶理论，我们描述了"鲁棒YES"与"鲁棒NO"实例的集合，并通过实数一阶理论允许量词消去这一特性，证明了这些集合是半代数的。