离散动力系统的O-极小不变量
O-Minimal Invariants for Discrete-Time Dynamical Systems
摘要：
线性回路的终止性分析在计算机科学的许多领域中起着关键作用，包括程序验证和抽象解释。对于线性循环的最简单的变体，终止问题已经涉及到数论中的深开放问题，例如线性递归序列的Skolem和Positivity问题的可判定性，或者离散时间线性动力系统的等价可达性问题。在本文中，我们介绍了类的\emph{o-minimal invariants}，这是广泛的比以前考虑的，并研究了可判定性的存在和算法合成等不变量作为证书的非终止线性循环配备了一大类的停机条件。我们建立了两个主要的可判定性结果，其中一个条件Schanuel的猜想在超越数论。
英文摘要：
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 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
