2026-07-21T14:17:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9118 2024-03-06T10:43:24Z ddc:004 open_access

O-Minimal Invariants for Linear Loops Almagor, Shaull Chistikov, Dmitry Ouaknine, Joël Worrell, James Invariants linear loops linear dynamical systems non-termination o-minimality 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Shaull Almagor and Dmitry Chistikov and Joël Ouaknine and James Worrell 2018 Is Part Of LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2018.114 urn:nbn:de:0030-drops-91188 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.114 eng https://creativecommons.org/licenses/by/3.0/legalcode