Advertisement

Theory of Computing Systems

, Volume 63, Issue 5, pp 1027–1048 | Cite as

Complete Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem

  • Nathanaël FijalkowEmail author
  • Pierre Ohlmann
  • Joël Ouaknine
  • Amaury Pouly
  • James Worrell
Article
  • 37 Downloads
Part of the following topical collections:
  1. Special Issue on Theoretical Aspects of Computer Science (STACS 2017)

Abstract

The Orbit Problem consists of determining, given a matrix A on \(\mathbb {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\(\mathcal {P} \subseteq \mathbb {R}^{d}\), i.e., sets that are stable under A and contain x but 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 succinct invariants of polynomial size. Our results imply that the class of closed semialgebraic invariants is closure-complete: there exists a closed semialgebraic invariant if and only if y is not in the topological closure of the orbit of x under A.

Keywords

Verification Algebraic computation Skolem Problem Orbit problem Invariants 

Notes

Acknowledgements

We would like to thank the reviewers for their very detailed and helpful comments, in particular pointing out a flaw in the complexity analysis in the first version of the paper.

References

  1. 1.
    Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry, Volume 36 of A Series of Modern Surveys in Mathematics. Springer, Berlin (1998)Google Scholar
  2. 2.
    Cai, J.-Y.: Computing Jordan Normal Forms Exactly for Commuting Matrices in Polynomial Time. Technical report, SUNY at Buffalo (2000)Google Scholar
  3. 3.
    Cassels, J.W.S.: An Introduction to Diophantine Approximation. Cambridge University Press, Cambridge (1965)zbMATHGoogle Scholar
  4. 4.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84–96. ACM Press (1978)Google Scholar
  5. 5.
    Cai, J.-Y., Lipton, R.J., Zalcstein, Y.: The complexity of the A B C problem. SIAM J. Comput. 29(6), 1878–1888 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Colón, M.: Polynomial approximations of the relational semantics of imperative programs. Sci. Comput. Program. 64(1), 76–96 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    van den Dries, LPD: Tame Topology and O-minimal Structures. London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge (1998)CrossRefzbMATHGoogle Scholar
  8. 8.
    Ge, G.: Testing equalities of multiplicative representations in polynomial time. In: SFCS, pp. 422–426. IEEE Computer Society (1993)Google Scholar
  9. 9.
    Harrison, M.A.: Lectures on Linear Sequential Machines. Academic Press, New York-Londres (1969)zbMATHGoogle Scholar
  10. 10.
    Kannan, R., Lipton, R.J.: The orbit problem is decidable. In: STOC, pp. 252–261 (1980)Google Scholar
  11. 11.
    Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM 33(4), 808–821 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Masser, D.W.: Linear relations on algebraic groups. In: Baker, A. (ed.) New Advances in Transcendence Theory, pp 248–262. Cambridge University Press, Cambridge (1988)Google Scholar
  13. 13.
    Mignotte, M.: Some useful bounds. In: Computer Algebra, Volume 4 of Computing Supplementum 4. Springer, Vienna (1982)Google Scholar
  14. 14.
    Müller-Olm, M., Seidl, H.: A note on Karr’s algorithm. In: ICALP, Volume 3142 of Lecture Notes in Computer Science, pp. 1016–1028. Springer (2004)Google Scholar
  15. 15.
    Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL, pp. 330–341. ACM (2004)Google Scholar
  16. 16.
    Ouaknine, J., Worrell, J.: Ultimate positivity is decidable for simple linear recurrence sequences. In: ICALP, pp. 330–341 (2014)Google Scholar
  17. 17.
    Tao, T.: Structure and Randomness. AMS (2008)Google Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2019

Authors and Affiliations

  1. 1.CNRSLaBRIBordeauxFrance
  2. 2.The Alan Turing Institute of data science and artificial intelligenceLondonUK
  3. 3.IRIFUniversité Paris Diderot - Paris 7ParisFrance
  4. 4.Max Planck Institute for Software Systems (MPI-SWS)Saarland Informatics CampusSaarbrückenGermany
  5. 5.Department of Computer ScienceOxford UniversityOxfordUK

Personalised recommendations