## Invariants for continuous linear dynamical systems

*Shaull Almagor*, *Edon Kelmendi*,
*Joël
Ouaknine*, and *James Worrell*
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 synthesising 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.

*Proceedings of ICALP 20*, LIPIcs 168, 2020. 22 pages.

PDF
© 2020 Shaull Almagor, Edon Kelmendi, Joël Ouaknine, and James Worrell.

Imprint / Data Protection