Exploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals

Abstrakt

In this paper, we consider an analysis of temporal properties of hybrid systems based on simulations, so-called falsification of requirements. We present a novel exploration-based algorithm for falsification of black-box models of hybrid systems based on the Voronoi bias. This approach is inspired by techniques used originally in motion planning: rapidly exploring random trees. Instead of commonly employed exploration that is based on coverage of inputs, the proposed exploration algorithm aims to explore possible outputs directly. It achieves that by covering a feature space that is associated with some spatial and temporal properties of output signals. This approach also does not require robustness or other guidance metrics tied to a specific behavior that is being falsified. This allows our algorithm to falsify specifications for which robustness is not conclusive enough to guide the falsification procedure.