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对应于多项式长度多项式微分方程的解。我们的论证表明，答案由精度决定：空间对应所涉及的精度。