Reachability in robust dynamical systems proven PSPACE-complete complexity
PSPACE-Completeness of the Reachability Relation of Robust Dynamical Systems
Computational Complexity
Summary
The problem of deciding if one state can be reached from another in a dynamical system is important but often very hard to solve. The authors study this problem for systems that are robust, meaning they tolerate small errors, and show it falls into a complexity class called PSPACE-complete. This means the problem is as hard as the toughest problems solvable with limited memory but is still computationally manageable in theory. Their work also tightens connections between models of continuous computation and complexity theory.
What this means in practice
- •For control system engineers: Design verification tools that analyze whether certain states can be reached in robust control systems within predictable resource bounds.
- •For automated verification developers: Create analysis frameworks for discrete and continuous dynamical models grounded in computable real-number complexity to improve software tools.
A theory result. No direct application yet.
Authors
Manon Blanc
Abstract
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.