License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.15
URN: urn:nbn:de:0030-drops-128278
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12827/
Go to the corresponding LIPIcs Volume Portal

Neumann, Eike ; Ouaknine, Joël ; Worrell, James

On Ranking Function Synthesis and Termination for Polynomial Programs

pdf-format:
LIPIcs-CONCUR-2020-15.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{neumann_et_al:LIPIcs:2020:12827,
  author =	{Eike Neumann and Jo{\"e}l Ouaknine and James Worrell},
  title =	{{On Ranking Function Synthesis and Termination for Polynomial Programs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{15:1--15:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Igor Konnov and Laura Kov{\'a}cs},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12827},
  URN =		{urn:nbn:de:0030-drops-128278},
  doi =		{10.4230/LIPIcs.CONCUR.2020.15},
  annote =	{Keywords: Semi-algebraic sets, Polynomial ranking functions, Polynomial programs}
}

Keywords: Semi-algebraic sets, Polynomial ranking functions, Polynomial programs
Collection: 31st International Conference on Concurrency Theory (CONCUR 2020)
Issue Date: 2020
Date of publication: 26.08.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI