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 presentation we focus on the decision problem of whether the solution of a system of linear differential equations 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 satisfying a given linear differential equation have infinitely many zeros on the non-negative reals? In our publication at LICS’16, we establish decidability in the case of a differential equation of order at most 7. On the other hand, in the same paper 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. In this presentation, we will offer a high-level overview of the problem, followed by an outline of the techniques from model theory and transcendental number theory which proved most useful in establishing our results.

Authors

• Ventsislav Chonev

Keywords

No keywords are indexed for this paper.