Verification and Falsification of Continuous and Hybrid Dynamical Systems

Tommaso Dreossi

Dipartimento Electrical Engineering and Computer Science di UC Berkeley

In this talk, we address the problem of determining whether a given dynamical system satisfies a requirement expressed in terms of unsafe regions or Signal Temporal Logic specifications. We will focus on polynomial dynamical systems and more complex hybrid systems (such as Simulink models). The presented methods include reachability analysis techniques based on Bernstein polynomials as well as black-box methods involving rapidly exploring random trees.