2026-07-28T01:18:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19390 2024-03-06T11:03:55Z ddc:004 open_access

Robust Positivity Problems for Linear Recurrence Sequences: The Frontiers of Decidability for Explicitly Given Neighbourhoods Vahanwala, Mihir Dynamical Systems Verification Robustness Linear Recurrence Sequences Positivity Ultimate Positivity Linear Recurrence Sequences (LRS) are a fundamental mathematical primitive for a plethora of applications such as the verification of probabilistic systems, model checking, computational biology, and economics. Positivity (are all terms of the given LRS non-negative?) and Ultimate Positivity (are all but finitely many terms of the given LRS non-negative?) 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. However, the state of the art is ill-equipped to reason about imprecision when its extent is explicitly specified. In this paper, we consider Robust Positivity and Ultimate Positivity problems where the neighbourhood of the initialisation, expressed 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 are unable to handle for general LRS would entail significant number-theoretic breakthroughs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mihir Vahanwala 2023 Is Part Of LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2023.17 urn:nbn:de:0030-drops-193909 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.17 eng https://creativecommons.org/licenses/by/4.0/legalcode