Document Open Access Logo

On Robustness for the Skolem and Positivity Problems

Authors S. Akshay , Hugo Bazille, Blaise Genest, Mihir Vahanwala

PDF
Thumbnail PDF

File

LIPIcs.STACS.2022.5.pdf
  • Filesize: 1.15 MB
  • 20 pages

Document Identifiers

Author Details

S. Akshay
  • Indian Institute of Technology Bombay, Mumbai, India
Hugo Bazille
  • Laboratoire de Recherche et Développement de l'Epita (LRDE), Rennes, France
Blaise Genest
  • Univ Rennes, CNRS, IRISA, France
Mihir Vahanwala
  • Indian Institute of Technology Bombay, Mumbai, India

Funding

This work was partly supported by the DST/CEFIPRA/INRIA associated team EQuaVE, DST/SERB Matrices grant MTR/2018/00074, and ANR-20-CE25-0012 MAVeriQ.

Cite As Get BibTex

S. Akshay, Hugo Bazille, Blaise Genest, and Mihir Vahanwala. On Robustness for the Skolem and Positivity Problems. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.STACS.2022.5

Abstract

The Skolem problem is a long-standing open problem in linear dynamical systems: can a linear recurrence sequence (LRS) ever reach 0 from a given initial configuration? Similarly, the positivity problem asks whether the LRS stays positive from an initial configuration. Deciding Skolem (or positivity) has been open for half a century: The best known decidability results are for LRS with special properties (e.g., low order recurrences). On the other hand, these problems are much easier for "uninitialized" variants, where the initial configuration is not fixed but can vary arbitrarily: checking if there is an initial configuration from which the LRS stays positive can be decided by polynomial time algorithms (Tiwari in 2004, Braverman in 2006).
In this paper, we consider problems that lie between the initialized and uninitialized variant. More precisely, we ask if 0 (resp. negative numbers) can be avoided from every initial configuration in a neighborhood of a given initial configuration. This can be considered as a robust variant of the Skolem (resp. positivity) problem. We show that these problems lie at the frontier of decidability: if the neighborhood is given as part of the input, then robust Skolem and robust positivity are Diophantine-hard, i.e., solving either would entail major breakthrough in Diophantine approximations, as happens for (non-robust) positivity. Interestingly, this is the first Diophantine-hardness result on a variant of the Skolem problem, to the best of our knowledge. On the other hand, if one asks whether such a neighborhood exists, then the problems turn out to be decidable in their full generality, with PSPACE complexity. Our analysis is based on the set of initial configurations such that positivity holds, which leads to new insights into these difficult problems, and interesting geometrical interpretations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Skolem problem
  • verification
  • dynamical systems
  • robustness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Manindra Agrawal, S. Akshay, Blaise Genest, and P. S. Thiagarajan. Approximate verification of the symbolic dynamics of Markov chains. J. ACM, 62(1):2:1-2:34, 2015. Google Scholar
  2. S. Akshay, Nikhil Balaji, Aniket Murhekar, Rohith Varma, and Nikhil Vyas. Near-Optimal Complexity Bounds for Fragments of the Skolem Problem. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020), volume 154, pages 37:1-37:18, 2020. Google Scholar
  3. S. Akshay, Nikhil Balaji, and Nikhil Vyas. Complexity of restricted variants of skolem and related problems. In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, August 21-25, 2017 - Aalborg, Denmark, volume 83 of LIPIcs, pages 78:1-78:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  4. S. Akshay, Blaise Genest, Bruno Karelovic, and Nikhil Vyas. On regularity of unary probabilistic automata. In STACS'16, pages 8:1-8:14. LIPIcs, 2016. Google Scholar
  5. S. Akshay, Blaise Genest, and Nikhil Vyas. Distribution-based objectives for Markov Decision Processes. In 33rf Symposium on Logic in Computer Science (LICS 2018), volume IEEE, pages 36-45, 2018. Google Scholar
  6. 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
  7. S. Basu, R. Pollack, and M. F. Roy. Algorithms in Real Algebraic Geometry. Springer, 2nd edition, 2006. Google Scholar
  8. Jean Berstel and Maurice Mignotte. Deux propriétés décidables des suites récurrentes linéaires. Bulletin de la Société Mathématique de France, 104:175-184, 1976. Google Scholar
  9. Manuel Biscaia, David Henriques, and Paulo Mateus. Decidability of approximate Skolem problem and applications to logical verification of dynamical properties of markov chains. ACM Trans. Comput. Logic, 16(1), December 2014. Google Scholar
  10. Vincent Blondel and Natacha Portier. The presence of a zero in an integer linear recurrent sequence is NP-hard to decide. Linear algebra and its Applications, 351:91-98, 2002. Google Scholar
  11. N. Bourbaki. Elements of Mathematics: General Topology (Part 2). Addison-Wesley, 1966. Google Scholar
  12. Mark Braverman. Termination of integer linear programs. In International Conference on Computer Aided Verification, pages 372-385. Springer, 2006. Google Scholar
  13. Ventsislav Chonev, Joël Ouaknine, and James Worrell. On the Skolem problem for continuous linear dynamical systems. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), pages 100:1-100:13. LIPIcs, 2016. Google Scholar
  14. H. Cohen. A Course in Computational Algebraic Number Theory. Springer-Verlag, 1993. Google Scholar
  15. 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
  16. Graham Everest, Alfred J. van der Poorten, Igor E. Shparlinski, and Thomas Ward. Recurrence Sequences. In Mathematical surveys and monographs, 2003. Google Scholar
  17. 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
  18. Kurt Mahler. Eine arithmetische Eigenschaft der Taylor-koeffizienten rationaler Funktionen. Noord-Hollandsche Uitgevers Mij, 1935. Google Scholar
  19. David W. Masser. Linear relations on algebraic groups. In New Advances in Transcendence Theory. Cambridge University Press, 1988. Google Scholar
  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. Thoralf Skolem. Ein Verfahren zur Behandlung gewisser exponentialer Gleichungen, 8de Skand. mat. Kongr. Forh. Stockholm, 1934. Google Scholar
  28. Ashish Tiwari. Termination of linear programs. In Computer-Aided Verification, CAV, volume 3114 of LNCS, pages 70-82. Springer, July 2004. Google Scholar
  29. Nikolai Vereshchagin. The problem of appearance of a zero in a linear recurrence sequence. Mat. Zametki, 38(2):609-615, 1985. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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