  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.
