Invariants for Continuous Linear Dynamical Systems
Invariants for Continuous Linear Dynamical Systems
复制标题
DOI：
10.4230/lipics.icalp.2020.107
复制
发表时间：
2020-04
期刊：
影响因子：
--
通讯作者：
Shaull Almagor;Edon Kelmendi;Joël Ouaknine;J. Worrell
中科院分区：
文献类型：
--
作者：
Shaull Almagor;Edon Kelmendi;Joël Ouaknine;J. Worrell
连续线性动力系统在数学、计算机科学、物理学和工程学中被广泛用于模拟系统随时间的演化。一个核心的技术，以证明这种系统的安全性能是通过合成归纳不变量。这是找到一组状态的任务，该状态在系统的动态下是封闭的，并且与给定的一组错误状态不相交。本文研究了在真实的数域的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.