On Recurrent Reachability for Continuous Linear Dynamical Systems

Abstract

The continuous evolution of a wide variety of systems, including continuous-time Markov chains and linear hybrid automata, can be described in terms of linear differential equations. In this paper we study the decision problem of whether the solution $\mathbf{x}(t)$ of a system of linear differential equations $d\mathbf{x}/dt=A\mathbf{x}$ reaches a target halfspace infinitely often. This recurrent reachability problem can equivalently be formulated as the following Infinite Zeros Problem: does a real-valued function $f:{\mathbb{R}}_{\ge 0}\to \mathbb{R}$ satisfying a given linear differential equation have infinitely many zeros? Our main decidability result is that if the differential equation has order at most $7$, then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order $9$ (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision.

Full version of paper at LICS'16