On recurrent reachability for continuous linear dynamical systems

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...

Celý popis

Podrobná bibliografie
Hlavní autoři: Ouaknine, J, Chonev, V, Worrell, J
Médium: Conference item
Vydáno: Association for Computing Machinery 2016
_version_ 1826281270386098176
author Ouaknine, J
Chonev, V
Worrell, J
author_facet Ouaknine, J
Chonev, V
Worrell, J
author_sort Ouaknine, J
collection OXFORD
description 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.
first_indexed 2024-03-07T00:26:17Z
format Conference item
id oxford-uuid:7e40a52e-1b71-4fb0-b58e-053f0b04d4f0
institution University of Oxford
last_indexed 2024-03-07T00:26:17Z
publishDate 2016
publisher Association for Computing Machinery
record_format dspace
spelling oxford-uuid:7e40a52e-1b71-4fb0-b58e-053f0b04d4f02022-03-26T21:08:55ZOn recurrent reachability for continuous linear dynamical systemsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:7e40a52e-1b71-4fb0-b58e-053f0b04d4f0Symplectic Elements at OxfordAssociation for Computing Machinery2016Ouaknine, JChonev, VWorrell, JThe 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.
spellingShingle Ouaknine, J
Chonev, V
Worrell, J
On recurrent reachability for continuous linear dynamical systems
title On recurrent reachability for continuous linear dynamical systems
title_full On recurrent reachability for continuous linear dynamical systems
title_fullStr On recurrent reachability for continuous linear dynamical systems
title_full_unstemmed On recurrent reachability for continuous linear dynamical systems
title_short On recurrent reachability for continuous linear dynamical systems
title_sort on recurrent reachability for continuous linear dynamical systems
work_keys_str_mv AT ouakninej onrecurrentreachabilityforcontinuouslineardynamicalsystems
AT chonevv onrecurrentreachabilityforcontinuouslineardynamicalsystems
AT worrellj onrecurrentreachabilityforcontinuouslineardynamicalsystems