The Library
O-minimal invariants for linear loops
Tools
Almagor, Shaull, Chistikov, Dmitry, Ouaknine, Joel and Worrell, James (2018) O-minimal invariants for linear loops. In: ICALP 2018: 45th International Colloquium on Automata, Languages, and Programming, Prague, Czech Republic, 9-13 Jul 2018. Published in: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018), 107 114:1-114:14. ISBN 9783959770767. doi:10.4230/LIPIcs.ICALP.2018.114 ISSN 1868-8969.
|
PDF
WRAP-O-minimal-invariants-for-linear-loops-Chistikov-2018.pdf - Published Version - Requires a PDF viewer. Available under License Creative Commons Attribution. Download (577Kb) | Preview |
Official URL: http://doi.org/10.4230/LIPIcs.ICALP.2018.114
Abstract
The termination analysis of linear loops plays a key role in several areas of computer science, including program verification and abstract interpretation. Such deceptively simple questions also relate to a number of deep open problems, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this paper, we introduce the class of \emph{o-minimal invariants}, which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel's conjecture.
Item Type: | Conference Item (Paper) | |||||||||
---|---|---|---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | |||||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | |||||||||
Library of Congress Subject Headings (LCSH): | Invariants, Dynamics, Algorithms | |||||||||
Series Name: | Leibniz International Proceedings in Informatics (LIPIcs) | |||||||||
Journal or Publication Title: | 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) | |||||||||
Publisher: | Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik | |||||||||
Place of Publication: | Germany | |||||||||
ISBN: | 9783959770767 | |||||||||
ISSN: | 1868-8969 | |||||||||
Official Date: | 2018 | |||||||||
Dates: |
|
|||||||||
Volume: | 107 | |||||||||
Page Range: | 114:1-114:14 | |||||||||
DOI: | 10.4230/LIPIcs.ICALP.2018.114 | |||||||||
Status: | Peer Reviewed | |||||||||
Publication Status: | Published | |||||||||
Access rights to Published version: | Open Access (Creative Commons) | |||||||||
Date of first compliant deposit: | 4 May 2018 | |||||||||
Date of first compliant Open Access: | 4 May 2018 | |||||||||
RIOXX Funder/Project Grant: |
|
|||||||||
Conference Paper Type: | Paper | |||||||||
Title of Event: | ICALP 2018: 45th International Colloquium on Automata, Languages, and Programming | |||||||||
Type of Event: | Conference | |||||||||
Location of Event: | Prague, Czech Republic | |||||||||
Date(s) of Event: | 9-13 Jul 2018 | |||||||||
Related URLs: | ||||||||||
Open Access Version: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year