In this paper we solve the problem of finding a trajectory that shows that a given hybrid dynamical system with deterministic evolution leaves a given set of states considered to be safe. The algorithm combines local with global search for achieving both efficiency and global convergence. In local search, it exploits derivatives for efficient computation. Unlike other methods for falsification of hybrid systems with deterministic evolution, we do not restrict our search to trajectories of a certain bounded length but search for error trajectories of arbitrary length.
The falsification problem can also be viewed as a boundary value problem which is a classical topic in numerical mathematics @cite_20 . However, classical numerical methods assume a fixed final time, whereas we search for error trajectories of arbitrary length. Moreover, classical methods for boundary values problems are restricted to purely continuous systems and the formulation of boundary conditions as equalities. Note that, unlike the continuous case, the trajectory of a hybrid system can reach a point @math for which @math holds every reaching a point @math for which @math holds.
@cite_20
1568666422
We present an algorithm for falsifying safety properties of hybrid systems, i.e., for finding a trajectory to an unsafe state. The 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 verification 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.