O-Minimal Invariants for Discrete-Time Dynamical Systems

TL;DR

This paper introduces o-minimal invariants as a new approach to analyze the termination of linear loops, connecting program verification with deep problems in number theory and establishing new decidability results.

Contribution

It defines the class of o-minimal invariants for linear loops and studies their decidability and synthesis, extending previous methods and linking to open problems in number theory.

Findings

Decidability results for the existence of o-minimal invariants

Conditional decidability based on Schanuel's conjecture

Broader class of invariants for termination analysis

Abstract

Termination analysis of linear loops plays a key r\^{o}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 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 in transcendental number theory.