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!
first_indexed 2022-06-07T12:31:22Z
last_indexed 2023-01-11T14:41:54Z
id cronfa60141
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2022-10-31T14:32:07.6523656</datestamp><bib-version>v2</bib-version><id>60141</id><entry>2022-06-07</entry><title>On Ranking Function Synthesis and Termination for Polynomial Programs</title><swanseaauthors><author><sid>1bf535eaa8d6fcdfbd464a511c1c0c78</sid><firstname>Eike</firstname><surname>Neumann</surname><name>Eike Neumann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2022-06-07</date><deptcode>SCS</deptcode><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>31st International Conference on Concurrency Theory (CONCUR 2020)</journal><volume>171</volume><journalNumber/><paginationStart/><paginationEnd/><publisher>Schloss Dagstuhl -- Leibniz-Zentrum f&#xFC;r Informatik</publisher><placeOfPublication/><isbnPrint/><isbnElectronic>978-3-95977-160-3</isbnElectronic><issnPrint/><issnElectronic>1868-8969</issnElectronic><keywords>Semi-algebraic sets, Polynomial ranking functions, Polynomial programs</keywords><publishedDay>26</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2020</publishedYear><publishedDate>2020-08-26</publishedDate><doi>10.4230/LIPIcs.CONCUR.2020.15</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders>Jo&#xEB;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.</funders><projectreference/><lastEdited>2022-10-31T14:32:07.6523656</lastEdited><Created>2022-06-07T13:23:34.5477947</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Eike</firstname><surname>Neumann</surname><order>1</order></author><author><firstname>Jo&#xEB;l</firstname><surname>Ouaknine</surname><order>2</order></author><author><firstname>James</firstname><surname>Worrell</surname><order>3</order></author></authors><documents><document><filename>60141__24405__0a0ed5bc2b3e4072adc017829d382c95.pdf</filename><originalFilename>60141.pdf</originalFilename><uploaded>2022-06-28T14:36:30.7751825</uploaded><type>Output</type><contentLength>446707</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>&#xA9; Eike Neumann, Jo&#xEB;l Ouaknine, and James Worrell; licensed under Creative Commons License CC-BY</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/3.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling 2022-10-31T14:32:07.6523656 v2 60141 2022-06-07 On Ranking Function Synthesis and Termination for Polynomial Programs 1bf535eaa8d6fcdfbd464a511c1c0c78 Eike Neumann Eike Neumann true false 2022-06-07 SCS 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. Conference Paper/Proceeding/Abstract 31st International Conference on Concurrency Theory (CONCUR 2020) 171 Schloss Dagstuhl -- Leibniz-Zentrum für Informatik 978-3-95977-160-3 1868-8969 Semi-algebraic sets, Polynomial ranking functions, Polynomial programs 26 8 2020 2020-08-26 10.4230/LIPIcs.CONCUR.2020.15 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 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. 2022-10-31T14:32:07.6523656 2022-06-07T13:23:34.5477947 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Eike Neumann 1 Joël Ouaknine 2 James Worrell 3 60141__24405__0a0ed5bc2b3e4072adc017829d382c95.pdf 60141.pdf 2022-06-28T14:36:30.7751825 Output 446707 application/pdf Version of Record true © Eike Neumann, Joël Ouaknine, and James Worrell; licensed under Creative Commons License CC-BY true eng https://creativecommons.org/licenses/by/3.0/
title On Ranking Function Synthesis and Termination for Polynomial Programs
spellingShingle On Ranking Function Synthesis and Termination for Polynomial Programs
Eike Neumann
title_short On Ranking Function Synthesis and Termination for Polynomial Programs
title_full On Ranking Function Synthesis and Termination for Polynomial Programs
title_fullStr On Ranking Function Synthesis and Termination for Polynomial Programs
title_full_unstemmed On Ranking Function Synthesis and Termination for Polynomial Programs
title_sort On Ranking Function Synthesis and Termination for Polynomial Programs
author_id_str_mv 1bf535eaa8d6fcdfbd464a511c1c0c78
author_id_fullname_str_mv 1bf535eaa8d6fcdfbd464a511c1c0c78_***_Eike Neumann
author Eike Neumann
author2 Eike Neumann
Joël Ouaknine
James Worrell
format Conference Paper/Proceeding/Abstract
container_title 31st International Conference on Concurrency Theory (CONCUR 2020)
container_volume 171
publishDate 2020
institution Swansea University
isbn 978-3-95977-160-3
issn 1868-8969
doi_str_mv 10.4230/LIPIcs.CONCUR.2020.15
publisher Schloss Dagstuhl -- Leibniz-Zentrum für Informatik
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description 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.
published_date 2020-08-26T04:18:00Z
_version_ 1763754199505436672
score 11.035634

Similar Items