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 $\delta$-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.

翻译：实数域上的离散时间或连续时间动力系统的验证已知是不可判定的。然而，已知不可判定性对某些系统类不成立：如果将鲁棒性定义为可达性关系在无穷小扰动下保持稳定，则其可达性关系是可判定的。换言之，不可判定性蕴含对无穷小扰动的敏感性——这一性质通常在实际考虑的系统中所不被期待，因此可（在一定程度上非正式地）视为理论中始终假设精确性所产生的伪象。类似地，已知实数域上的逻辑公式具有不可判定性，但若考虑δ-不可判定性（需判定某性质为真，或与真值相差δ）则不再成立。我们首先将前述结论扩展至一般动力系统（包括离散时间、连续时间乃至混合系统）的理论框架，并关联两种研究途径。同时将鲁棒性与可达性关系的若干几何性质相联系。但核心在于：当系统具有鲁棒性时，量化其扰动水平便具有理论意义。我们证明：若假设精度受多项式扰动仍保持鲁棒性，则可达性验证可达复杂度类PSPACE，甚至可刻画该复杂度类。若假设轨迹的时间或长度受多项式扰动仍保持鲁棒性，则可得类似结论，但复杂度类为PTIME。近期意外发现，多项式常微分方程解的长度对应于计算时间：PTIME对应于多项式长度解的多项式微分方程。我们的结果论证：答案由精度给出——空间对应所涉及的精度。