Document Open Access Logo

On Ranking Function Synthesis and Termination for Polynomial Programs

Authors Eike Neumann, Joël Ouaknine, James Worrell

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.15.pdf
  • Filesize: 436 kB
  • 15 pages

Document Identifiers

Author Details

Eike Neumann
  • Department of Computer Science, Oxford University, UK
Joël Ouaknine
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
  • 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 DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
  • Worrell, James: Supported by EPSRC Fellowship EP/N008197/1.

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.CONCUR.2020.15

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
Keywords
  • Semi-algebraic sets
  • Polynomial ranking functions
  • Polynomial programs

Metrics

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

References

  1. Amir M. Ben-Amram, Jesús J. Doménech, and Samir Genaim. Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets. In Bor-Yuh Evan Chang, editor, Static Analysis, pages 459-480. Springer International Publishing, 2019. 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 and Samir Genaim. Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions. In Computer Aided Verification, volume 9207 of Lecture Notes in Computer Science, pages 304-321. Springer, 2015. Google Scholar
  4. Amir M. Ben-Amram and Samir Genaim. On Multiphase-Linear Ranking Functions. In Computer Aided Verification - 29th International Conference, CAV 2017, volume 10427 of Lecture Notes in Computer Science, pages 601-620. Springer, 2017. Google Scholar
  5. Jacek Bochnak, Michel Coste, and Marie-Françoise Roy. Real Algebraic Geometry. Springer-Verlag Berlin Heidelberg, 1998. Google Scholar
  6. Mark Braverman. Termination of Integer Linear Programs. In Computer Aided Verification, 18th International Conference, CAV, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 372-385. Springer, 2006. Google Scholar
  7. Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. Termination Analysis of Probabilistic Programs Through Positivstellensatz’s. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 3-22. Springer, 2016. Google Scholar
  8. Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, and Chaochen Zhou. Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems. In Theoretical Aspects of Computing - ICTAC 2007, 4th International Colloquium, 2007, Proceedings, volume 4711 of Lecture Notes in Computer Science, pages 34-49. Springer, 2007. Google Scholar
  9. Byron Cook, Abigail See, and Florian Zuleger. Ramsey vs. Lexicographic Termination Proving. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, volume 7795 of Lecture Notes in Computer Science, pages 47-61. Springer, 2013. 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, Proceedings, volume 3385 of Lecture Notes in Computer Science, pages 1-24. Springer, 2005. Google Scholar
  11. Florian Frohn, Marcel Hark, and Jürgen Giesl. On the Decidability of Termination for Polynomial Loops. CoRR, abs/1910.11588, 2019. URL: http://arxiv.org/abs/1910.11588.
  12. Mehran Hosseini, Joël Ouaknine, and James Worrell. Termination of Linear Loops over the Integers. In 46th International Colloquium on Automata, Languages, and Programming, ICALP, volume 132 of LIPIcs, pages 118:1-118:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  13. Yi Li. Termination of Single-Path Polynomial Loop Programs. In Theoretical Aspects of Computing - ICTAC, Proceedings, volume 9965 of Lecture Notes in Computer Science, pages 33-50, 2016. Google Scholar
  14. Yi Li, Wenyuan Wu, and Yong Feng. On ranking functions for single-path linear-constraint loops. Int J Softw Tools Technol Transfer, 2019. URL: https://doi.org/10.1007/s10009-019-00549-9.
  15. Joël Ouaknine and James Worrell. Positivity Problems for Low-Order Linear Recurrence Sequences. In Chandra Chekuri, editor, Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, Portland, Oregon, USA, January 5-7, 2014, pages 366-379. SIAM, 2014. Google Scholar
  16. Andreas Podelski and Andrey Rybalchenko. A Complete Method for the Synthesis of Linear Ranking Functions. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Proceedings, volume 2937 of Lecture Notes in Computer Science, pages 239-251. Springer, 2004. Google Scholar
  17. Ashish Tiwari. Termination of Linear Programs. In Rajeev Alur and Doron A. Peled, editors, Computer Aided Verification, 16th International Conference, CAV 2004, Proceedings, volume 3114 of Lecture Notes in Computer Science, pages 70-82. Springer, 2004. Google Scholar
  18. Caterina Urban. The Abstract Domain of Segmented Ranking Functions. In Static Analysis - 20th International Symposium, SAS 2013, Proceedings, volume 7935 of Lecture Notes in Computer Science, pages 43-62. Springer, 2013. Google Scholar
  19. Bican Xia and Zhihai Zhang. Termination of linear programs with nonlinear constraints. Journal of Symbolic Computation, 45(11):1234-1249, 2010. URL: https://doi.org/10.1016/j.jsc.2010.06.006.
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact