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.
Proceedings of CONCUR 20, LIPIcs 171, 2020. 15 pages.
PDF
© 2020 Eike Neumann, Joël Ouaknine, and James Worrell.