Local Descent For Temporal Logic Falsification of Cyber-Physical Systems (Extended Technical Report)

TL;DR

This paper introduces a local descent method combined with simulated annealing to improve the efficiency of falsifying cyber-physical systems modeled as hybrid automata by minimizing a robustness metric.

Contribution

It presents a novel hybrid approach that integrates local gradient descent with global search for more effective falsification of hybrid automata.

Findings

Enhanced ability to find unsafe behaviors in hybrid automata.

Improved efficiency over purely heuristic methods.

Demonstrated effectiveness on benchmark systems.

Abstract

One way to analyze Cyber-Physical Systems is by modeling them as hybrid automata. Since reachability analysis for hybrid nonlinear automata is a very challenging and computationally expensive problem, in practice, engineers try to solve the requirements falsification problem. In one method, the falsification problem is solved by minimizing a robustness metric induced by the requirements. This optimization problem is usually a non-convex non-smooth problem that requires heuristic and analytical guidance to be solved. In this paper, functional gradient descent for hybrid systems is utilized for locally decreasing the robustness metric. The local descent method is combined with Simulated Annealing as a global optimization method to search for unsafe behaviors.