Invariants for Continuous Linear Dynamical Systems

Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. Yet, fundamental reachability problems for this class of systems are not known to be decidable. In this paper we study invariant synthesis for continuous linear dynamic systems. This is the task of finding a set that contains the orbit of the system, is itself invariant under the dynamics, and is disjoint from the a given set of error configurations. Assuming Schanuel's conjecture in transcendental number theory, we establish effective synthesis for o-minimal invariants and semi-algebraic error sets. Without Schanuel's conjecture, we give a procedure for synthesizing semi-algebraic invariants that contain all but a bounded initial segment of the orbit and are disjoint from the error set. We further prove that unconditional 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.