文章基本信息

标题：Invariants for Continuous Linear Dynamical Systems
本地全文：下载
作者：Shaull Almagor ; Edon Kelmendi ; Jo{"e}l Ouaknine 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：168
页码：107:1-107:15
DOI：10.4230/LIPIcs.ICALP.2020.107
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Invariants; continuous linear dynamical systems; continuous Skolem problem; safety; o-minimality