Quantifiying the robustness of dynamical systems: relating time and space to length and precision
Time: 14:00 -- Location: LRI, 445
summary: Reasoning about dynamical systems evolving over the reals is well-known
to lead to undecidability. In particular, it is known there cannot be decision
procedures for first-order theories over the reals, or decision procedures for state reachability.
However, various results in the literature have shown that decision procedures exist
when restricting to robust systems, with a suitably-chosen notion
of robustness. In particular, in verification, it has been established that if the
state reachability is not sensitive to infinitesimal perturbations, then decision
procedures for state reachability exist.
Here, we first propose a unified theory explaining in a uniform
framework these statements, that were established in different contexts. We prove that robustness to
some precision is inherently related to the complexity of the decision procedure:
When a system is robust, it makes sense to quantify at which level of perturbation it is.
We prove that assuming robustness to a polynomial perturbation
on precision leads to PSPACE and even to a characterisation of PSPACE. We
prove that assuming robustness to polynomial perturbation on time or length
leads to similar statements for PTIME.
These statements can also be interpreted in relation with several
recent results about the computational power of analogue models of computation.