Document Open Access Logo

Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem

Authors Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell



PDF
Thumbnail PDF

File

LIPIcs.STACS.2017.29.pdf
  • Filesize: 463 kB
  • 13 pages

Document Identifiers

Author Details

Nathanaël Fijalkow
Pierre Ohlmann
Joël Ouaknine
Amaury Pouly
James Worrell

Cite AsGet BibTex

Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell. Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 29:1-29:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.STACS.2017.29

Abstract

The Orbit Problem consists of determining, given a linear transformation A on d-dimensional rationals Q^d, together with vectors x and y, whether the orbit of x under repeated applications of A can ever reach y. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s. In this paper, we are concerned with the problem of synthesising suitable invariants P which are subsets of R^d, i.e., sets that are stable under A and contain x and not y, thereby providing compact and versatile certificates of non-reachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable invariants of polynomial size. It is worth noting that the existence of semilinear invariants, on the other hand, is (to the best of our knowledge) not known to be decidable.
Keywords
  • Verification,algebraic computation,Skolem Problem,Orbit Problem,invariants

Metrics

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

References

  1. Jin-Yi Cai. Computing Jordan normal forms exactly for commuting matrices in polynomial time. Technical report, SUNY at Buffalo, 2000. Google Scholar
  2. Jin-Yi Cai, Richard J. Lipton, and Yechezkel Zalcstein. The complexity of the A B C problem. SIAM J. Comput., 29(6):1878-1888, 2000. URL: http://dx.doi.org/10.1137/S0097539794276853.
  3. John W. S. Cassels. An introduction to Diophantine approximation. Cambridge University Press, 1965. Google Scholar
  4. Ventsislav Chonev, Joël Ouaknine, and James Worrell. On the complexity of the Orbit Problem. Journal of the ACM, 63(3):23, 2016. URL: http://dx.doi.org/10.1145/2857050.
  5. L. P. D. van den Dries. Tame Topology and O-minimal Structures. London Mathematical Society Lecture Note Series. Cambridge University Press, May 1998. Google Scholar
  6. G. Ge. Testing equalities of multiplicative representations in polynomial time. In Proceedings of SFCS, pages 422-426. IEEE Computer Society, 1993. Google Scholar
  7. Michael A. Harrison. Lectures on linear sequential machines. New York-Londres, Academic Press, 1969. Google Scholar
  8. Ravindran Kannan and Richard J. Lipton. The Orbit Problem is decidable. In Proceedings of STOC, pages 252-261, 1980. URL: http://dx.doi.org/10.1145/800141.804673.
  9. Ravindran Kannan and Richard J. Lipton. Polynomial-time algorithm for the Orbit Problem. Journal of the ACM, 33(4):808-821, 1986. URL: http://dx.doi.org/10.1145/6490.6496.
  10. David W. Masser. Linear relations on algebraic groups. In Alan Baker, editor, New Advances in Transcendence Theory, pages 248-262. Cambridge University Press, 1988. URL: http://dx.doi.org/10.1017/CBO9780511897184.016.
  11. Joël Ouaknine and James Worrell. Ultimate positivity is decidable for simple linear recurrence sequences. In Proceedings of ICALP, pages 330-341, 2014. URL: http://dx.doi.org/10.1007/978-3-662-43951-7_28.
  12. Terence Tao. Structure and Randomness. AMS, 2008. 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