No Cover Image

Conference Paper/Proceeding/Abstract 1089 views 163 downloads

On Ranking Function Synthesis and Termination for Polynomial Programs

Eike Neumann Orcid Logo, Joël Ouaknine, James Worrell

31st International Conference on Concurrency Theory (CONCUR 2020), Volume: 171

Swansea University Author: Eike Neumann Orcid Logo

  • 60141.pdf

    PDF | Version of Record

    © Eike Neumann, Joël Ouaknine, and James Worrell; licensed under Creative Commons License CC-BY

    Download (436.24KB)

Check full text

DOI (Published version): 10.4230/LIPIcs.CONCUR.2020.15

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 s...

Full description

Published in: 31st International Conference on Concurrency Theory (CONCUR 2020)
ISBN: 978-3-95977-160-3
ISSN: 1868-8969
Published: Schloss Dagstuhl -- Leibniz-Zentrum für Informatik 2020
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa60141
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.
Keywords: Semi-algebraic sets, Polynomial ranking functions, Polynomial programs
College: Faculty of Science and Engineering
Funders: Joël Ouaknine: Supported by ERC grant AVS-ISS (648701) and DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science). James Worrell: Supported by EPSRC Fellowship EP/N008197/1.

Similar Items