On recurrent reachability for continuous linear dynamical systems Conference Paper

Author(s): Chonev, Ventsislav; Ouaknine, Joël; Worrell, James
Title: On recurrent reachability for continuous linear dynamical systems
Affiliation IST Austria
Abstract: 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 dx/dt = Ax 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: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.
Keywords: reachability; Differential equations; linear dynamical systems; Diophantine Approximation; Skolem problem
Conference Title: LICS: Logic in Computer Science
Volume: 515
Issue 524
Conference Dates: 5 - 8 July, 2016
Conference Location: New York, USA
ISBN: 978-147998875-4
Publisher: IEEE  
Date Published: 2016-01-01
Start Page: 515
End Page: 524
DOI: 10.1145/2933575.2934548
Notes: Ventsislav Chonev is supported by Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and ERC Advanced Grant (267989: QUAREM). Jo ̈ el Ouaknine is supported by ERC grant AVS-ISS (648701). James Worrell is supported by EPSRC grant EP/N008197/1
Open access: yes (repository)
IST Austria Authors
  1. Ventsislav Chonev
    3 Chonev
Related IST Austria Work