Manon Blanc (LIX, Ecole Polytechnique)

Reasoning about dynamical systems evolving over the reals is well-known to lead to undecidability. 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. More fundamentally, while all these statements are only about computability issues, we also consider complexity theory aspects. We prove that robustness to some precision is inherently related to the complexity of the decision procedure.

The full preprint can be found at : https://arxiv.org/pdf/2301.12723.pdf