2026-07-23T19:13:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12514 2024-03-06T10:50:20Z ddc:004 open_access

Invariants for Continuous Linear Dynamical Systems Almagor, Shaull Kelmendi, Edon Ouaknine, Joël Worrell, James Invariants continuous linear dynamical systems continuous Skolem problem safety o-minimality 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Shaull Almagor and Edon Kelmendi and Joël Ouaknine and James Worrell 2020 Is Part Of LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2020.107 urn:nbn:de:0030-drops-125141 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.107 eng https://creativecommons.org/licenses/by/3.0/legalcode