连续线性动力系统的不变量
Invariants for Continuous Linear Dynamical Systems
摘要：
连续线性动力系统在数学、计算机科学、物理学和工程学中被广泛用于模拟系统随时间的演化。一个核心的技术，以证明这种系统的安全性能是通过合成归纳不变量。这是找到一组状态的任务，该状态在系统的动态下是封闭的，并且与给定的一组错误状态不相交。在本文中，我们研究的问题，合成归纳不变量是定义在O-最小的扩展有序域的实数。特别是，假设Schanuel的猜想在超越数论中，我们建立了有效的合成的o-最小不变量的情况下，半代数错误集。在不使用Schanuel猜想的情况下，我们给出了一个合成O-极小不变量的过程，该不变量包含轨道的所有有界初始段，并且与给定的半代数错误集不相交。我们进一步证明了包含整个轨道的半代数不变量的有效合成至少和超越数论中的某个公开问题一样困难。
英文摘要：
Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. A central technique for certifying safety properties of such systems is by synthesising inductive invariants. This is the task of finding a set of states that is closed under the dynamics of the system and is disjoint from a given set of error states. In this paper we study the problem of synthesising inductive invariants that are definable in o-minimal expansions of the ordered field of real numbers. In particular, assuming Schanuel's conjecture in transcendental number theory, we establish effective synthesis of o-minimal invariants in the case of semi-algebraic error sets. Without using Schanuel's conjecture, we give a procedure for synthesizing o-minimal invariants that contain all but a bounded initial segment of the orbit and are disjoint from a given semi-algebraic error set. We further prove that effective synthesis of semi-algebraic invariants that contain the whole orbit, is at least as hard as a certain open problem in transcendental number theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
