Document Open Access Logo

The Semialgebraic Orbit Problem

Authors Shaull Almagor, Joël Ouaknine, James Worrell

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2019.6.pdf
  • Filesize: 0.51 MB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Computing methodologies → Algebraic algorithms
  • Theory of computation → Logic and verification
Keywords
  • linear dynamical systems
  • Orbit Problem
  • first order theory of the reals

Metrics

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

Abstract

The Semialgebraic Orbit Problem is a fundamental reachability question that arises in the analysis of discrete-time linear dynamical systems such as automata, Markov chains, recurrence sequences, and linear while loops. An instance of the problem comprises a dimension d in N, a square matrix A in Q^{d x d}, and semialgebraic source and target sets S,T subseteq R^d. The question is whether there exists x in S and n in N such that A^nx in T. 
The main result of this paper is that the Semialgebraic Orbit Problem is decidable for dimension d <= 3. Our decision procedure relies on separation bounds for algebraic numbers as well as a classical result of transcendental number theory - Baker’s theorem on linear forms in logarithms of algebraic numbers. We moreover argue that our main result represents a natural limit to what can be decided (with respect to reachability) about the orbit of a single matrix. On the one hand, semialgebraic sets are arguably the largest general class of subsets of R^d for which membership is decidable. On the other hand, previous work has shown that in dimension d=4, giving a decision procedure for the special case of the Orbit Problem with singleton source set S and polytope target set T would entail major breakthroughs in Diophantine approximation.

Cite As Get BibTex

Shaull Almagor, Joël Ouaknine, and James Worrell. The Semialgebraic Orbit Problem. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.STACS.2019.6

Author Details

Shaull Almagor
  • Department of Computer Science, Oxford University, UK
Joël Ouaknine
  • Max Planck Institute for Software Systems, Germany \and Department of Computer Science, Oxford University, UK
James Worrell
  • Department of Computer Science, Oxford University, UK

Funding

  • Ouaknine, Joël: Supported by ERC grant AVS-ISS (648701), and by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - Projektnummer 389792660 - TRR 248.
  • Worrell, James: Supported by EPSRC Fellowship EP/N008197/1.

References

  1. S. Almagor, J. Ouaknine, and J. Worrell. The Polytope-Collision Problem. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, pages 24:1-24:14, 2017. Google Scholar
  2. A. Baker and G. Wüstholz. Logarithmic forms and group varieties. J. reine angew. Math, 442(19-62):3, 1993. Google Scholar
  3. S. Basu, R. Pollack, and M-F. Roy. Algorithms in real algebraic geometry, volume 20033. Springer, 2005. Google Scholar
  4. V. Chonev, J. Ouaknine, and J. Worrell. The polyhedron-hitting problem. In Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, pages 940-956. SIAM, 2015. Google Scholar
  5. V. Chonev, J. Ouaknine, and J. Worrell. On the Complexity of the Orbit Problem. J. ACM, 63(3):23:1-23:18, 2016. Google Scholar
  6. H. Cohen. A course in computational algebraic number theory, volume 138. Springer Science &Business Media, 2013. Google Scholar
  7. G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, May 20-23, 1975, pages 134-183. Springer, 1975. Google Scholar
  8. F.R. Gantmacher. The Theory of Matrices. Number v. 2 in The Theory of Matrices. Chelsea Publishing Company, 1959. Google Scholar
  9. V. Halava, T. Harju, M. Hirvensalo, and J. Karhumäki. Skolem’s Problem - On the Border between Decidability and Undecidability. Technical Report 683, Turku Centre for Computer Science, 2005. Google Scholar
  10. M. A Harrison. Lectures on linear sequential machines. Technical report, DTIC Document, 1969. Google Scholar
  11. R. Kannan and R. J. Lipton. Polynomial-time algorithm for the orbit problem. Journal of the ACM (JACM), 33(4):808-821, 1986. Google Scholar
  12. G. Lafferriere, G. J. Pappas, and S. Yovine. Symbolic Reachability Computation for Families of Linear Vector Fields. J. Symb. Comput., 32(3):231-253, 2001. Google Scholar
  13. M. Mignotte. Some useful bounds. In Computer algebra, pages 259-263. Springer, 1983. Google Scholar
  14. M. Mignotte, T. Shorey, and R. Tijdeman. The distance between terms of an algebraic recurrence sequence. J. für die reine und angewandte Math., 349, 1984. Google Scholar
  15. M. Müller-Olm and H. Seidl. Computing polynomial program invariants. Inf. Process. Lett., 91(5):233-244, 2004. Google Scholar
  16. J. Ouaknine and J. 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
  17. V. Y. Pan. Optimal and nearly optimal algorithms for approximating polynomial zeros. Computers &Mathematics with Applications, 31(12):97-138, 1996. Google Scholar
  18. J. Renegar. A Faster PSPACE Algorithm for Deciding the Existential Theory of the Reals. In 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988, pages 291-295, 1988. Google Scholar
  19. J. 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. Journal of symbolic computation, 13(3):255-299, 1992. Google Scholar
  20. T. Tao. Structure and randomness: pages from year one of a mathematical blog. American Mathematical Soc., 2008. Google Scholar
  21. A. Tarski. A decision method for elementary algebra and geometry. Rand Corporation, 1951. Google Scholar
  22. N. K. Vereshchagin. Occurrence of zero in a linear recursive sequence. Mathematical notes of the Academy of Sciences of the USSR, 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact