Document Open Access Logo

Robust Positivity Problems for Linear Recurrence Sequences: The Frontiers of Decidability for Explicitly Given Neighbourhoods

Author Mihir Vahanwala

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2023.17.pdf
  • Filesize: 0.95 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Dynamical Systems
  • Verification
  • Robustness
  • Linear Recurrence Sequences
  • Positivity
  • Ultimate Positivity

Metrics

Abstract

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.

Cite As Get BibTex

Mihir Vahanwala. Robust Positivity Problems for Linear Recurrence Sequences: The Frontiers of Decidability for Explicitly Given Neighbourhoods. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSTTCS.2023.17

Author Details

Mihir Vahanwala
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany

Funding

The author is partially funded by DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).

Acknowledgements

This work is an extension of a recent collaboration with S Akshay, Hugo Bazille, and Blaise Genest. I am especially grateful to Valérie Berthé for her help in number-theoretic aspects of the paper. Our discussions took place during the Bellairs Dynamical Systems workshop organised by my advisor, Joël Ouaknine. I thank Bellairs Research Institute of McGill University, Barbados, for the hospitality and peaceful environment conducive to scientific discussion. Finally, I thank all the anonymous reviewers for their astute observations and constructive suggestions.

References

  1. S. Akshay, Nikhil Balaji, Aniket Murhekar, Rohith Varma, and Nikhil Vyas. Near-Optimal Complexity Bounds for Fragments of the Skolem Problem. In Christophe Paul and Markus Bläser, editors, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020), volume 154 of Leibniz International Proceedings in Informatics (LIPIcs), pages 37:1-37:18, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2020.37.
  2. S. Akshay, Hugo Bazille, Blaise Genest, and Mihir Vahanwala. On robustness for the skolem and positivity problems. In STACS 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.STACS.2022.5.
  3. S. Akshay, Hugo Bazille, Blaise Genest, and Mihir Vahanwala. On robustness for the skolem, positivity and ultimate positivity problems, 2022. URL: https://arxiv.org/abs/2211.02365.
  4. S. Akshay, Blaise Genest, and Nikhil Vyas. Distribution-based objectives for Markov Decision Processes. In 33rd Symposium on Logic in Computer Science (LICS 2018), volume IEEE, pages 36-45, 2018. Google Scholar
  5. Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, and Markus A. Whiteland. Reachability in dynamical systems with rounding. In Nitin Saxena and Sunil Simon, editors, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, volume 182 of LIPIcs, pages 36:1-36:17, 2020. Google Scholar
  6. S. Basu, R. Pollack, and M. F. Roy. Algorithms in Real Algebraic Geometry. Springer, 2nd edition, 2006. Google Scholar
  7. Valérie Berthé and Jungwon Lee. Dynamics of ostrowski skew-product: I. limit laws and hausdorff dimensions, 2022. URL: https://arxiv.org/abs/2108.06780.
  8. Avraham Bourla. The ostrowski expansions revealed, 2016. URL: https://arxiv.org/abs/1605.07992.
  9. Mark Braverman. Termination of integer linear programs. In International Conference on Computer Aided Verification, pages 372-385. Springer, 2006. Google Scholar
  10. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. In 2008 21st IEEE Computer Security Foundations Symposium, pages 51-65, 2008. URL: https://doi.org/10.1109/CSF.2008.7.
  11. H. Cohen. A Course in Computational Algebraic Number Theory. Springer-Verlag, 1993. Google Scholar
  12. Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, Sadegh Soudjani, and James Worrell. The pseudo-Skolem problem is decidable. In Filippo Bonchi and Simon J. Puglisi, editors, 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, volume 202 of LIPIcs, pages 34:1-34:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  13. Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, and James Worrell. The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), volume 241 of Leibniz International Proceedings in Informatics (LIPIcs), pages 40:1-40:13, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.40.
  14. Manuel Eberl and René Thiemann. Factorization of polynomials with algebraic coefficients. Archive of Formal Proofs, November 2021. Formal proof development. URL: https://isa-afp.org/entries/Factor_Algebraic_Polynomial.html.
  15. Graham Everest, Alfred J. van der Poorten, Igor E. Shparlinski, and Thomas Ward. Recurrence Sequences. In Mathematical surveys and monographs, 2003. Google Scholar
  16. Vesa Halava, Tero Harju, Mika Hirvensalo, and Juhani Karhumäki. Skolem’s problem - On the border between decidability and undecidability. Technical Report 683, Turku Centre for Computer Science, 2005. Google Scholar
  17. A Khintchine. Neuer beweis und verallgemeinerung eines hurwitzschen satzes. Mathematische Annalen, 111:631-637, 1935. Google Scholar
  18. J. C. Lagarias and J. O. Shallit. Linear fractional transformations of continued fractions with bounded partial quotients. Journal de théorie des nombres de Bordeaux, 9:267-279, 1997. Google Scholar
  19. Richard Lipton, Florian Luca, Joris Nieuwveld, Joël Ouaknine, David Purser, and James Worrell. On the skolem problem and the skolem conjecture. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3533328.
  20. M. Mignotte. Some useful bounds. In Computer Algebra, 1982. Google Scholar
  21. Maurice Mignotte, Tarlok Nath Shorey, and Robert Tijdeman. The distance between terms of an algebraic recurrence sequence. Journal für die reine und angewandte Mathematik, 349:63-76, 1984. Google Scholar
  22. Eike Neumann. Decision problems for linear recurrences involving arbitrary real numbers. Logical Methods in Computer Science, 17(3), 2021. Google Scholar
  23. Joël Ouaknine and James Worrell. On the positivity problem for simple linear recurrence sequences. In International Colloquium on Automata, Languages, and Programming, pages 318-329. Springer, 2014. Google Scholar
  24. Joël Ouaknine and James Worrell. Positivity problems for low-order linear recurrence sequences. In Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, Portland, Oregon, USA, January 5-7, 2014, pages 366-379. SIAM, 2014. Google Scholar
  25. Joël Ouaknine and James Worrell. Ultimate positivity is decidable for simple linear recurrence sequences. In International Colloquium on Automata, Languages, and Programming, pages 330-341. Springer, 2014. Google Scholar
  26. James Renegar. On the Computational Complexity and Geometry of the First-Order Theory of the Reals, Part I: Introduction. Preliminaries. The Geometry of Semi-Algebraic Sets. The Decision Problem for the Existential Theory of the Reals. J. Symb. Comput., 13:255-300, 1992. Google Scholar
  27. Ashish Tiwari. Termination of linear programs. In Computer-Aided Verification, CAV, volume 3114 of LNCS, pages 70-82. Springer, July 2004. Google Scholar
  28. Nikolai Vereshchagin. The problem of appearance of a zero in a linear recurrence sequence. Mat. Zametki, 38(2):609-615, 1985. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact