PSPACE-Completeness of the Reachability Relation of Robust Dynamical Systems

Overview & Synopsis

Dynamical systems are a widely used model of computation and an intuitive representation of many natural phenomena in many applied fields. The last decades have seen an impressive use of computers in studying and analysing them, with several visible theoretical breakthroughs. The question of reachability for dynamical systems is central: given two points, is there a trajectory between them in the dynamical system? Reachability, in particular over the reals, is undecidable in the general case: it is only computably enumerable, even under reasonable hypotheses, e.g. for a computable dynamics in general. But it is known to become decidable, and even lies in PSPACE, under suitably quantified robustness assumptions. In this paper, we focus on PSPACE-completeness results over the reals, in the sense of computable analysis, regarding discrete-time and continuous-time robust dynamical systems. We prove that, under some additional and rather reasonable hypotheses, the reachability relation becomes even PSPACE-complete for both classical and second-order complexity second-order complexity, for an adapted notion of reduction. As a side-effect, we also prove an improvement of an algebraic Ordinary Differential Equations-based characterisation of PSPACE, removing one of the base functions of the algebra. By doing so, we link results from dynamical systems and complexity over the reals, including the models of computable analysis and second-order complexity.