The Library
O-minimal invariants for linear loops
Tools
Tools
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. ISSN 1868-8969. doi:10.4230/LIPIcs.ICALP.2018.114
|
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 | |||||||||
| 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
