## On ranking function synthesis and termination for polynomial programs

*Eike Neumann*, *Joël
Ouaknine*, and *James Worrell*
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.

Imprint / Data Protection