Document Open Access Logo

O-Minimal Invariants for Linear Loops

Authors Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, James Worrell

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2018.114.pdf
  • Filesize: 0.6 MB
  • 14 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Computing methodologies → Algebraic algorithms
  • Theory of computation → Logic and verification
Keywords
  • Invariants
  • linear loops
  • linear dynamical systems
  • non-termination
  • o-minimality

Metrics

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

Abstract

The termination analysis of linear loops plays a key rôle in several areas of computer science, including program verification and abstract interpretation. Such deceptively simple questions also relate to a number of deep open problems, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this paper, we introduce the class of o-minimal invariants, which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel's conjecture in transcendental number theory.

Cite As Get BibTex

Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, and James Worrell. O-Minimal Invariants for Linear Loops. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 114:1-114:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ICALP.2018.114

Author Details

Shaull Almagor
  • Department of Computer Science, Oxford University, UK
Dmitry Chistikov
  • Centre for Discrete Mathematics and its Applications (DIMAP) & , Department of Computer Science, University of Warwick, UK
Joël Ouaknine
  • Max Planck Institute for Software Systems, Germany & , Department of Computer Science, Oxford University, UK
James Worrell
  • Department of Computer Science, Oxford University, UK

Funding

  • Ouaknine, Joël: Joël Ouaknine was supported by ERC grant AVS-ISS (648701)
  • Worrell, James: James Worrell was supported by EPSRC Fellowship EP/N008197/1.

References

  1. Alan Baker and Gisbert Wüstholz. Logarithmic forms and group varieties. J. reine angew. Math, 442(19-62):3, 1993. Google Scholar
  2. Amir M. Ben-Amram and Samir Genaim. Ranking functions for linear-constraint loops. J. ACM, 61(4):26:1-26:55, 2014. Google Scholar
  3. Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the termination of integer loops. ACM Trans. Program. Lang. Syst., 34(4):16:1-16:24, 2012. Google Scholar
  4. Mark Braverman. Termination of integer linear programs. In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pages 372-385, 2006. Google Scholar
  5. John W.S. Cassels. An Introduction to Diophantine Approximation. Cambridge University Press, 1965. Google Scholar
  6. Ventsislav Chonev, Joël Ouaknine, and James Worrell. The Orbit Problem in higher dimensions. In Symposium on Theory of Computing Conference, STOC'13, Palo Alto, CA, USA, June 1-4, 2013, pages 941-950, 2013. Google Scholar
  7. Ventsislav Chonev, Joël Ouaknine, and James Worrell. The polyhedron-hitting problem. In Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2015, San Diego, CA, USA, January 4-6, 2015, pages 940-956, 2015. Google Scholar
  8. Ventsislav Chonev, Joël Ouaknine, and James Worrell. On the complexity of the orbit problem. J. ACM, 63(3):23:1-23:18, 2016. Google Scholar
  9. Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, pages 420-432, 2003. Google Scholar
  10. Patrick Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings, pages 1-24, 2005. Google Scholar
  11. Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pages 84-96, 1978. Google Scholar
  12. L. P. D. van den Dries. Tame Topology and O-minimal Structures. London Mathematical Society Lecture Note Series. Cambridge University Press, 1998. Google Scholar
  13. 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, March 8-11, 2017, Hannover, Germany, pages 29:1-29:13, 2017. Google Scholar
  14. Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, and Ru-Gang Xu. Proving non-termination. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 147-158, 2008. Google Scholar
  15. Ravindran Kannan and Richard J. Lipton. The orbit problem is decidable. In Proceedings of the 12th Annual ACM Symposium on Theory of Computing, April 28-30, 1980, Los Angeles, California, USA, pages 252-261, 1980. Google Scholar
  16. Ravindran Kannan and Richard J. Lipton. Polynomial-time algorithm for the orbit problem. J. ACM, 33(4):808-821, 1986. Google Scholar
  17. Zachary Kincaid, John Cyphert, Jason Breck, and Thomas W. Reps. Non-linear reasoning for invariant synthesis. PACMPL, 2(POPL):54:1-54:33, 2018. Google Scholar
  18. Angus Macintyre and Alex J. Wilkie. On the decidability of the real exponential field. In Piergiorgio Odifreddi, editor, Kreiseliana. About and Around Georg Kreisel, pages 441-467. A K Peters, 1996. Google Scholar
  19. David W Masser. Linear relations on algebraic groups. New Advances in Transcendence Theory, pages 248-262, 1988. Google Scholar
  20. 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
  21. Joël Ouaknine, João Sousa Pinto, and James Worrell. On termination of integer linear loops. In Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2015, San Diego, CA, USA, January 4-6, 2015, pages 957-969, 2015. Google Scholar
  22. Joël Ouaknine and James Worrell. On the positivity problem for simple linear recurrence sequences,. In Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, pages 318-329, 2014. Google Scholar
  23. 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, 2014. Google Scholar
  24. 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
  25. Joël Ouaknine and James Worrell. On linear recurrence sequences and loop termination. SIGLOG News, 2(2):4-13, 2015. Google Scholar
  26. Enric Rodríguez-Carbonell and Deepak Kapur. An abstract interpretation approach for automatic generation of polynomial invariants. In Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings, pages 280-295, 2004. Google Scholar
  27. Enric Rodríguez-Carbonell and Deepak Kapur. Generating all polynomial invariants in simple loops. J. Symb. Comput., 42(4):443-476, 2007. Google Scholar
  28. Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Non-linear loop invariant generation using gröbner bases. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pages 318-329, 2004. Google Scholar
  29. T. Tao. Structure and randomness: pages from year one of a mathematical blog. American Mathematical Society, 2008. Google Scholar
  30. Alfred Tarski. A decision method for elementary algebra and geometry. Bulletin of the American Mathematical Society, 59, 1951. Google Scholar
  31. Ashish Tiwari. Termination of linear programs. In Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, pages 70-82, 2004. Google Scholar
  32. N. K. Vereshchagin. The problem of appearance of a zero in a linear recurrence sequence (in Russian). Mat. Zametki, 38(2), 1985. Google Scholar
  33. A. J. Wilkie. Model completeness results for expansions of the ordered field of real numbers by restricted pfaffian functions and the exponential function. Journal of the American Mathematical Society, 9(4):1051-1094, 1996. Google Scholar
  34. Bican Xia and Zhihai Zhang. Termination of linear programs with nonlinear constraints. J. Symb. Comput., 45(11):1234-1249, 2010. 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