NExG: Provable and Guided State Space Exploration of Neural Network Control Systems using Sensitivity Approximation

TL;DR

This paper introduces NExG, a novel sensitivity approximation-based method for guided state space exploration of neural network controlled systems, improving trajectory generation and falsification of temporal logic specifications.

Contribution

It presents a new sensitivity approximation technique for guided exploration, with a theoretical framework ensuring target neighborhood reachability, and demonstrates superior performance over existing methods.

Findings

Outperforms previous state space exploration techniques

Achieves higher quality and faster convergence in trajectory generation

Enhances falsification of temporal logic specifications

Abstract

We propose a new technique for performing state space exploration of closed loop control systems with neural network feedback controllers. Our approach involves approximating the sensitivity of the trajectories of the closed loop dynamics. Using such an approximator and the system simulator, we present a guided state space exploration method that can generate trajectories visiting the neighborhood of a target state at a specified time. We present a theoretical framework which establishes that our method will produce a sequence of trajectories that will reach a suitable neighborhood of the target state. We provide thorough evaluation of our approach on various systems with neural network feedback controllers of different configurations. We outperform earlier state space exploration techniques and achieve significant improvement in both the quality (explainability) and performance (convergence rate). Finally, we adopt our algorithm for the falsification of a class of temporal logic specification, assess its performance against a state-of-the-art falsification tool, and show its potential in supplementing existing falsification algorithms.