Paper detail

On Recurrent Reachability for Continuous Linear Dynamical Systems

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 $\boldsymbol{x}(t)$ of a system of linear differential equations $d\boldsymbol{x}/dt=A\boldsymbol{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}_{\geq 0}\rightarrow\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.