Document

**Published in:** LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

We study the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets. We establish a uniform upper bound on the number of iterations it takes for every orbit of a rational matrix to escape a compact semialgebraic set defined over rational data. Our bound is doubly exponential in the ambient dimension, singly exponential in the degrees of the polynomials used to define the semialgebraic set, and singly exponential in the bitsize of the coefficients of these polynomials and the bitsize of the matrix entries. We show that our bound is tight by providing a matching lower bound.

Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, and James Worrell. Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 39:1-39:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dcosta_et_al:LIPIcs.MFCS.2022.39, author = {D'Costa, Julian and Lefaucheux, Engel and Neumann, Eike and Ouaknine, Jo\"{e}l and Worrell, James}, title = {{Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set}}, booktitle = {47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)}, pages = {39:1--39:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-256-3}, ISSN = {1868-8969}, year = {2022}, volume = {241}, editor = {Szeider, Stefan and Ganian, Robert and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.39}, URN = {urn:nbn:de:0030-drops-168374}, doi = {10.4230/LIPIcs.MFCS.2022.39}, annote = {Keywords: Discrete linear dynamical systems, Program termination, Compact semialgebraic sets, Uniform termination bounds} }

Document

**Published in:** LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

We study the computational complexity of the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets, or equivalently the Termination Problem for affine loops with compact semialgebraic guard sets. Consider the fragment of the theory of the reals consisting of negation-free ∃ ∀-sentences without strict inequalities. We derive several equivalent characterisations of the associated complexity class which demonstrate its robustness and illustrate its expressive power. We show that the Compact Escape Problem is complete for this class.

Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, and James Worrell. On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dcosta_et_al:LIPIcs.MFCS.2021.33, author = {D'Costa, Julian and Lefaucheux, Engel and Neumann, Eike and Ouaknine, Jo\"{e}l and Worrell, James}, title = {{On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets}}, booktitle = {46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)}, pages = {33:1--33:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-201-3}, ISSN = {1868-8969}, year = {2021}, volume = {202}, editor = {Bonchi, Filippo and Puglisi, Simon J.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.33}, URN = {urn:nbn:de:0030-drops-144734}, doi = {10.4230/LIPIcs.MFCS.2021.33}, annote = {Keywords: Discrete linear dynamical systems, Program termination, Compact semialgebraic sets, Theory of the reals} }

Document

Track A: Algorithms, Complexity and Games

**Published in:** LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

We study decision problems for sequences which obey a second-order holonomic recurrence of the form f(n + 2) = P(n) f(n + 1) + Q(n) f(n) with rational polynomial coefficients, where P is non-constant, Q is non-zero, and the degree of Q is smaller than or equal to that of P. We show that existence of infinitely many zeroes is decidable. We give partial algorithms for deciding the existence of a zero, positivity of all sequence terms, and positivity of all but finitely many sequence terms. If Q does not have a positive integer zero then our algorithms halt on almost all initial values (f(1), f(2)) for the recurrence. We identify a class of recurrences for which our algorithms halt for all initial values. We further identify a class of recurrences for which our algorithms can be extended to total ones.

Eike Neumann, Joël Ouaknine, and James Worrell. Decision Problems for Second-Order Holonomic Recurrences. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 99:1-99:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{neumann_et_al:LIPIcs.ICALP.2021.99, author = {Neumann, Eike and Ouaknine, Jo\"{e}l and Worrell, James}, title = {{Decision Problems for Second-Order Holonomic Recurrences}}, booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)}, pages = {99:1--99:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-195-5}, ISSN = {1868-8969}, year = {2021}, volume = {198}, editor = {Bansal, Nikhil and Merelli, Emanuela and Worrell, James}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.99}, URN = {urn:nbn:de:0030-drops-141682}, doi = {10.4230/LIPIcs.ICALP.2021.99}, annote = {Keywords: holonomic sequences, Positivity Problem, Skolem Problem} }

Document

**Published in:** LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

We consider the problem of synthesising polynomial ranking functions for single-path loops over the reals with continuous semi-algebraic update function and compact semi-algebraic guard set. We show that a loop of this form has a polynomial ranking function if and only if it terminates. We further show that termination is decidable for such loops in the special case where the update function is affine.

Eike Neumann, Joël Ouaknine, and James Worrell. On Ranking Function Synthesis and Termination for Polynomial Programs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{neumann_et_al:LIPIcs.CONCUR.2020.15, author = {Neumann, Eike and Ouaknine, Jo\"{e}l and Worrell, James}, title = {{On Ranking Function Synthesis and Termination for Polynomial Programs}}, booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)}, pages = {15:1--15:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-160-3}, ISSN = {1868-8969}, year = {2020}, volume = {171}, editor = {Konnov, Igor and Kov\'{a}cs, Laura}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.15}, URN = {urn:nbn:de:0030-drops-128278}, doi = {10.4230/LIPIcs.CONCUR.2020.15}, annote = {Keywords: Semi-algebraic sets, Polynomial ranking functions, Polynomial programs} }