## On recurrent reachability for continuous linear dynamical systems

*Ventsislav Chonev*,
*Joël
Ouaknine*, and *James Worrell*
The continuous evolution of a wide variety of systems, including
continous-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
*x*(*t*) of a system of linear differential
equations *d**x*/*dt* = *A**x*
reaches a target hyperplane infinitely often.
This recurrent reachability problem can equivalently be
formulated as the following Infinite Zeros Problem:
does a real-valued function
*f* : **R**_{>0} --> **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.

*Proceedings of LICS 16*, 2016. 12 pages.

PDF
© 2016 IEEE Computer Society Press.