Finding errors of hybrid systems by optimising an abstraction-based quality estimate

Abstract. We present an algorithm for falsifying safety properties of hybrid systems, i.e., for finding a trajectory to an unsafe state. The main approach is to approximate how close a point is to being an initial point of an error trajectory using a real-valued quality function, and then to use numerical optimisation to search for an optimum of this function. The function is computed by running simulations, where information coming from abstractions computed by a verifi-cation algorithm is exploited to determine whether a simulation looks promising and should be continued or cancelled. This information becomes more reliable as the abstraction becomes more refined. We thus interleave falsification and verification attempts. In contrast to related work, we consider hybrid systems with completely deterministic evolution. Note: This AVACS report is the extended version of a conference paper [44]. It contains some proof sketches, more background material, more details on experimental results, and more discussions of related work.