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

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 a 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, and show its potential in supplementing existing falsification algorithms.