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

TL;DR

This paper introduces a novel output-space exploration algorithm for falsifying hybrid system models, leveraging Voronoi bias to improve coverage without relying on robustness metrics, inspired by motion planning techniques.

Contribution

The paper presents a new exploration-based falsification algorithm for hybrid systems that operates directly in output space using Voronoi bias, avoiding reliance on robustness measures.

Findings

Effective in falsifying hybrid system specifications without robustness guidance

Outperforms existing tools in certain falsification scenarios

Operates efficiently on black-box models without detailed internal information

Abstract

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 in the output space. 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 algorithm aims to cover all possible outputs directly. Compared to other state-of-the-art falsification tools, it 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.