No Cover Image

Conference Paper/Proceeding/Abstract 629 views 45 downloads

On Ranking Function Synthesis and Termination for Polynomial Programs

Eike Neumann, Joël Ouaknine, James Worrell

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

Swansea University Author: Eike Neumann

  • 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
Tags: Add Tag
No Tags, Be the first to tag this record!
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