Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Gidon Ernst, Jiří Fejlek

TL;DR

The paper tackles falsification of temporal (STL) properties for black-box hybrid systems by moving exploration from the input space to the space of output signals. It introduces Output Space Exploration (OSE), an RRT-inspired method that uses Voronoi bias in a feature-based output-signal space to generate diverse counterexamples without relying on robustness guidance. Through extensive benchmarks (Simple Integrator, Automatic Transmission, Chasing Cars) and comparisons with uniform/nonuniform sampling, random walks, RRT, and optimization-based falsification (SHC, DE, CMA-ES), OSE demonstrates competitive performance and complementary strengths to NR, often handling specifications difficult for robustness-guided methods. The approach is implemented in MATLAB and shows promise as a practical tool for falsification, capable of tackling complex, multi-specification scenarios without heavy reliance on problem-specific guidance.

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.

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

TL;DR

The paper tackles falsification of temporal (STL) properties for black-box hybrid systems by moving exploration from the input space to the space of output signals. It introduces Output Space Exploration (OSE), an RRT-inspired method that uses Voronoi bias in a feature-based output-signal space to generate diverse counterexamples without relying on robustness guidance. Through extensive benchmarks (Simple Integrator, Automatic Transmission, Chasing Cars) and comparisons with uniform/nonuniform sampling, random walks, RRT, and optimization-based falsification (SHC, DE, CMA-ES), OSE demonstrates competitive performance and complementary strengths to NR, often handling specifications difficult for robustness-guided methods. The approach is implemented in MATLAB and shows promise as a practical tool for falsification, capable of tackling complex, multi-specification scenarios without heavy reliance on problem-specific guidance.

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.

Paper Structure

This paper contains 32 sections, 15 equations, 4 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Falsification: optimization and exploration
  3. Rapidly Exploring Random Trees
  4. RRT algorithm
  5. RRT and model falsification
  6. Exploration in the space of output signals
  7. Conceptual Algorithm
  8. Implementation
  9. Selection of feature levels.
  10. Generation of random features.
  11. Feature metric.
  12. Generation of random inputs.
  13. Computational experiments
  14. Benchmarks
  15. Simple Integrator
  16. ...and 17 more sections

Figures (4)

  • Figure 1: Rapidly exploring random tree (Algorithm 1)
  • Figure 2: Progress of Algorithm 1 for the simple integrator problem. The RRT algorithm will block itself from exploring further trajectories that cross those already seen, i.e., it will not be able to follow the indicated arrow.
  • Figure 3: Progress of OSE (Algorithm 3) for the simple integrator. Black-bordered points denote a feature by which the current output signal (blue) was selected. The second figure shows the falsifying output signal found by OSE.
  • Figure 4: Convergence of exploration algorithms: uniform random (UR, red), nonuniform random (NR, green), random walk (RW, yellow), random graph (RG, purple) , Algorithm 1 (RRT, dark blue), Output Space Exploration (OSE, light blue).