O-Minimal Invariants for Linear Loops
| Autor: | Almagor, S., Chistikov, D., Ouaknine, J., Worrell, J. |
|---|---|
| Přispěvatelé: | Wagner, Michael |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: | |
| Zdroj: | 45th International Colloquium on Automata, Languages, and Programming, ICALP 45th International Colloquium on Automata, Languages, and Programming Leibniz International Proceedings in Informatics |
| ISSN: | 1868-8969 |
| Popis: | 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 in transcendental number theory. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|