Linear Hybrid System Falsification With Descent

TL;DR

This paper introduces a local search method for hybrid automata falsification, formulated as a differentiable optimization problem and solved with SQP, enhancing stochastic algorithms in complex hybrid systems.

Contribution

It presents a novel local search approach for hybrid automata falsification using differentiable optimization and SQP, improving existing stochastic methods.

Findings

Local search improves falsification success rates.

Differentiable formulation enables efficient optimization.

Method effectively handles complex hybrid dynamics.

Abstract

In this paper, we address the problem of local search for the falsification of hybrid automata with affine dynamics. Namely, if we are given a sequence of locations and a maximum simulation time, we return the trajectory that comes the closest to the unsafe set. In order to solve this problem, we formulate it as a differentiable optimization problem which we solve using Sequential Quadratic Programming. The purpose of developing such a local search method is to combine it with high level stochastic optimization algorithms in order to falsify hybrid systems with complex discrete dynamics and high dimensional continuous spaces. Experimental results indicate that indeed the local search procedure improves upon the results of pure stochastic optimization algorithms.