The Skolem, Positivity, and Ultimate Positivity problems for Linear Recurrence Sequences (LRS) are number-theoretic problems whose decidability has been open for decades. They are known to be at least as hard as Diophantine approximation, an open number-theoretic problem. LRS have scientific applications ranging from theoretical biology to software verification and formal languages. Given the inherent imprecision and need for safety margins in the real world, we consider the problems for LRS with the following notion of robustness: does the sequence satisfy the required property despite small perturbations in the given initialisation? Although some interpretations of this notion yield problems that are still Diophantine hard, others can be shown to be decidable, in PSPACE even! In this talk, we discuss how the decision procedure strings together remarkable and profound results from computational algebra, number theory, and logic. The techniques we discuss are indeed a thematic feature of modern progress in this area, and we briefly sketch how they have been extended to handle more sophisticated semi-algebraic reachability sets, and to tackle the problem of invariant synthesis.
Bio: Mihir Vahanwala is a doctoral researcher at MPI-SWS, Saarbrücken. He works in the Foundations of Algorithmic Verification group led by Joël Ouaknine.
