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 continoustime 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 realvalued 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:

9781479988754

Publisher:

IEEE

Date Published:

20160101

Start Page: 
515

End Page:

524

URL: 

DOI: 
10.1145/2933575.2934548

Notes: 
Ventsislav Chonev is supported by Austrian
Science Fund (FWF) NFN Grant No S11407N23 (RiSE/SHiNE),
ERC Start grant (279307: Graph Games), and ERC Advanced
Grant (267989: QUAREM). Jo
̈
el Ouaknine is supported by ERC
grant AVSISS (648701). James Worrell is supported by EPSRC
grant EP/N008197/1

Open access: 
yes (repository) 