Conference item
On ranking function synthesis and termination for polynomial programs
- Abstract:
- 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.
- Publication status:
- Published
- Peer review status:
- Reviewed (other)
Actions
Access Document
- Files:
-
-
(Preview, Version of record, 436.2KB, Terms of use)
-
- Publisher copy:
- 10.4230/LIPIcs.CONCUR.2020.15
Authors
- Publisher:
- Leibniz International Proceedings in Informatics
- Journal:
- 31st International Conference on Concurrency Theory More from this journal
- Volume:
- 171
- Pages:
- 15:1-15:15
- Publication date:
- 2020-08-26
- Acceptance date:
- 2020-06-28
- Event title:
- 31st International Conference on Concurrency Theory
- DOI:
- ISSN:
-
1868-8969
- Language:
-
English
- Keywords:
- Pubs id:
-
1115279
- Local pid:
-
pubs:1115279
- Deposit date:
-
2020-07-01
Terms of use
- Copyright holder:
- Neumann et al.
- Copyright date:
- 2020
- Rights statement:
- © Eike Neumann, Joël Ouaknine, and James Worrell; licensed under Creative Commons License CC-BY
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record