On Recurrent Reachability for Continuous Linear Dynamical Systems
Ventsislav Chonev, Joel Ouaknine, James Worrell

TL;DR
This paper investigates the problem of determining whether solutions to linear differential equations reach a target repeatedly, establishing decidability for equations up to order 7 and linking higher orders to deep number theory challenges.
Contribution
It proves decidability of the recurrent reachability problem for linear systems of order at most 7 and connects higher-order cases to major open problems in Diophantine approximation.
Findings
Decidability established for systems up to order 7.
Higher orders (9 and above) relate to computing Lagrange constants.
Decision problem remains open for order 8.
Abstract
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 of a system of linear differential equations 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 satisfying a given linear differential equation have infinitely many zeros? Our main decidability result is that if the differential equation has order at most , then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order (and above)…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
Topicssemigroups and automata theory · Polynomial and algebraic computation · Formal Methods in Verification
