
arXiv: 1802.09263
Termination analysis of linear loops plays a key rôle in several areas of computer science, including program verification and abstract interpretation. Already for the simplest variants of linear loops the question of termination relates to deep open problems in number theory, 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 article, 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 is transcendental number theory.
FOS: Computer and information sciences, Computer Science - Computational Complexity, Computer Science - Logic in Computer Science, Mathematics - Algebraic Geometry, FOS: Mathematics, Computational Complexity (cs.CC), F.3.1, Algebraic Geometry (math.AG), QA76, Logic in Computer Science (cs.LO)
FOS: Computer and information sciences, Computer Science - Computational Complexity, Computer Science - Logic in Computer Science, Mathematics - Algebraic Geometry, FOS: Mathematics, Computational Complexity (cs.CC), F.3.1, Algebraic Geometry (math.AG), QA76, Logic in Computer Science (cs.LO)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 3 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
