Table of Contents
Fetching ...

Measuring robustness of dynamical systems. Relating time and space to length and precision

Manon Blanc, Olivier Bournez

TL;DR

This work develops a unified theory linking robustness of reachability under perturbations to classic complexity classes across discrete, continuous, and hybrid dynamical systems. By embedding computational models into dynamical systems and analyzing perturbations (space, time, and length), it shows that polynomial robustness corresponds to PSPACE, while time- and length-based perturbations correspond to PTIME, with precision acting as the resource that plays the role of space. The authors connect robustness with δ-decidability and provide a spectrum of results that extend known undecidability bounds to verifiable, complexity-bounded regimes, including computable analysis frameworks for non-rational updates and CA-based notions of drawability. These insights offer a principled view of why practical verification often succeeds despite worst-case undecidability and establish a concrete link between geometric reachability properties and computational complexity in analog models. The results have implications for the design of robust verification techniques and for understanding the fundamental limits of simulation and analysis in continuous-time and hybrid systems.

Abstract

Verification of discrete time or continuous time dynamical systems over the reals is known to be undecidable. It is however known that undecidability does not hold for various classes of systems: if robustness is defined as the fact that reachability relation is stable under infinitesimal perturbation, then their reachability relation is decidable. In other words, undecidability implies sensitivity under infinitesimal perturbation, a property usually not expected in systems considered in practice, and hence can be seen (somehow informally) as an artefact of the theory, that always assumes exactness. In a similar vein, it is known that, while undecidability holds for logical formulas over the reals, it does not hold when considering delta-undecidability: one must determine whether a property is true, or $δ$-far from being true. We first extend the previous statements to a theory for general (discrete time, continuous-time, and even hybrid) dynamical systems, and we relate the two approaches. We also relate robustness to some geometric properties of reachability relation. But mainly, when a system is robust, it then makes sense to quantify at which level of perturbation. We prove that assuming robustness to polynomial perturbations on precision leads to reachability verifiable in complexity class PSPACE, and even to a characterization of this complexity class. We prove that assuming robustness to polynomial perturbations on time or length of trajectories leads to similar statements, but with PTIME. It has been recently unexpectedly shown that the length of a solution of a polynomial ordinary differential equation corresponds to a time of computation: PTIME corresponds to solutions of polynomial differential equations of polynomial length. Our results argue that the answer is given by precision: space corresponds to the involved precision.

Measuring robustness of dynamical systems. Relating time and space to length and precision

TL;DR

This work develops a unified theory linking robustness of reachability under perturbations to classic complexity classes across discrete, continuous, and hybrid dynamical systems. By embedding computational models into dynamical systems and analyzing perturbations (space, time, and length), it shows that polynomial robustness corresponds to PSPACE, while time- and length-based perturbations correspond to PTIME, with precision acting as the resource that plays the role of space. The authors connect robustness with δ-decidability and provide a spectrum of results that extend known undecidability bounds to verifiable, complexity-bounded regimes, including computable analysis frameworks for non-rational updates and CA-based notions of drawability. These insights offer a principled view of why practical verification often succeeds despite worst-case undecidability and establish a concrete link between geometric reachability properties and computational complexity in analog models. The results have implications for the design of robust verification techniques and for understanding the fundamental limits of simulation and analysis in continuous-time and hybrid systems.

Abstract

Verification of discrete time or continuous time dynamical systems over the reals is known to be undecidable. It is however known that undecidability does not hold for various classes of systems: if robustness is defined as the fact that reachability relation is stable under infinitesimal perturbation, then their reachability relation is decidable. In other words, undecidability implies sensitivity under infinitesimal perturbation, a property usually not expected in systems considered in practice, and hence can be seen (somehow informally) as an artefact of the theory, that always assumes exactness. In a similar vein, it is known that, while undecidability holds for logical formulas over the reals, it does not hold when considering delta-undecidability: one must determine whether a property is true, or -far from being true. We first extend the previous statements to a theory for general (discrete time, continuous-time, and even hybrid) dynamical systems, and we relate the two approaches. We also relate robustness to some geometric properties of reachability relation. But mainly, when a system is robust, it then makes sense to quantify at which level of perturbation. We prove that assuming robustness to polynomial perturbations on precision leads to reachability verifiable in complexity class PSPACE, and even to a characterization of this complexity class. We prove that assuming robustness to polynomial perturbations on time or length of trajectories leads to similar statements, but with PTIME. It has been recently unexpectedly shown that the length of a solution of a polynomial ordinary differential equation corresponds to a time of computation: PTIME corresponds to solutions of polynomial differential equations of polynomial length. Our results argue that the answer is given by precision: space corresponds to the involved precision.
Paper Structure (11 sections, 51 theorems, 1 equation)

This paper contains 11 sections, 51 theorems, 1 equation.

Key Result

Lemma 1

Consider the following decision problem $\operatorname{PATH}(G,u,v)$: given a directed graph $G=(V,\rightarrow)$, and some vertices $u,v \in V$, determine whether there is some path between $u$ and $v$ in $G$, denoted by $u \stackrel{*}{\rightarrow} v$. Then $\operatorname{PATH}(G,u,v) \in \operator

Theorems & Definitions (101)

  • Lemma 1: Reachability for graphs
  • proof
  • Lemma 2: Immerman–Szelepcsényi's theorem immerman1988nondeterministicSzelepcsenyi
  • proof
  • Corollary 3
  • Theorem 4: Savitch's theorem
  • proof
  • Corollary 5
  • Remark 6
  • Definition 7: Discrete Time Dynamical System
  • ...and 91 more