On ranking function synthesis and termination for 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 s...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Leibniz International Proceedings in Informatics
2020
|
| Summary: | 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. |
|---|