Linear Recurrence Sequences (LRS) are a fundamental mathematical primitive for a plethora of applications such as model checking, probabilistic systems, computational biology, and economics. Positivity (are all terms of the given LRS at least 0?) and Ultimate Positivity (are all but finitely many terms of the given LRS at least 0?) 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. In this paper, we consider Robust Positivity and Ultimate Positivity problems where the neighbourhood of the initialisation, specified 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 can't handle would entail significant number-theoretic breakthroughs.
翻译:线性递归序列(LRS)是模型检测、概率系统、计算生物学和经济学等诸多应用中的基本数学原语。正性(给定LRS的所有项是否均非负?)与终极正性(给定LRS除有限项外的所有项是否均非负?)是数论中重要的未解决判定问题。近年来,这些问题的鲁棒版本(即:在初始值存在微小扰动时,LRS是否仍(终极)正?)作为应对实际场景中不确定性的建模工具,已受到广泛关注。本文考虑初始值邻域(以自然且通用的格式指定)同时作为输入的鲁棒正性与终极正性问题。我们通过证明严格的可判定性结果作出贡献:若算法能处理我们技术无法处理的阶数,则将导致数论领域的重大突破。