Conference item
O-minimal invariants for linear loops
- Abstract:
- The termination analysis of linear loops plays a key rôle 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 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Version of record, pdf, 615.7KB, Terms of use)
-
- Publisher copy:
- 10.4230/LIPIcs.ICALP.2018.114
Authors
- Publisher:
- Leibniz Center for Informatics
- Host title:
- 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)
- Journal:
- 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) More from this journal
- Publication date:
- 2018-06-29
- Acceptance date:
- 2018-04-19
- DOI:
- Keywords:
- Pubs id:
-
pubs:842323
- UUID:
-
uuid:ccc28084-53c3-4a01-b62c-29aa7bdfadee
- Local pid:
-
pubs:842323
- Source identifiers:
-
842323
- Deposit date:
-
2018-04-19
Terms of use
- Copyright holder:
- Ouaknine et al
- Copyright date:
- 2018
- Notes:
-
© Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, and James Worrell;
licensed under Creative Commons License CC-BY
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record