2026-07-25T09:51:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12827 2024-03-06T10:50:47Z ddc:004 open_access

On Ranking Function Synthesis and Termination for Polynomial Programs Neumann, Eike Ouaknine, Joël Worrell, James Semi-algebraic sets Polynomial ranking functions Polynomial programs 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Eike Neumann and Joël Ouaknine and James Worrell 2020 Is Part Of LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2020.15 urn:nbn:de:0030-drops-128278 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.15 eng https://creativecommons.org/licenses/by/3.0/legalcode