2015/07/13 by Ventsislav Chonev, Joël Ouaknine, Chonev, Ventsislav +3
Computer Science · #F.2.m #FOS: Electrical engineering #Formal Methods in Verification #Polynomial and algebraic computation #Systems and Control (eess.SY) #electronic engineering #information engineering #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1507.03632
openalex publication_date 2015/07/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 \boldsymbolx(t) of a system of linear differential equations d\boldsymbolx/dt=A\boldsymbolx 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:ℝ≥ 0→ℝ 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.