Invariants for continuous linear dynamical systems

Conference item

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.

Authors: Kelmendi, E; Ouaknine, J; Worrell, J; Almagor, S

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Schloss Dagstuhl
• Volume: 168
• Article number: 107
• Series: Leibniz International Proceedings in Informatics
• Publication date: 2020-06-29
• Acceptance date: 2020-04-15
• Event title: 47th International Colloquium on Automata Languages and Programming (ICALP 2020)
• Event start date: 2020-07-08
• Event end date: 2020-07-11
• DOI: 10.4230/LIPIcs.ICALP.2020.107
• ISSN: 1868-8969
• ISBN: 9783959771382
• Language: English
• Keywords: FFR; safety; continuous Skolem problem; o-minimality; invariants; continuous linear dynamical systems