On Ranking Function Synthesis and Termination for Polynomial Programs
On Ranking Function Synthesis and Termination for Polynomial Programs
复制标题
DOI：
10.4230/lipics.concur.2020.15
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
E. Neumann;Joël Ouaknine;J. Worrell
中科院分区：
文献类型：
--
作者：
E. Neumann;Joël Ouaknine;J. 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.