Sensitive State-Space Exploration

In this paper, we describe a simulation-based approach to the verification of high dimensional nonlinear systems subject to disturbances and uncertainty in the initial conditions. Standard simulation can only sample finitely many initial states and disturbance signals and cannot verify correctness in an exhaustive manner. The alternative approach of computing all the reachable states of the system using set-based simulation, can provide, in principle, correctness proofs but is computationally expensive especially for high dimensional and nonlinear systems. In this paper we propose an approach that provides a good compromise between set-based computation and simulation by combining guided random exploration of the state space together with sensitivity analysis. The exploration technique is used to choose input signals that guarantee good coverage of the reachable set, while sensitivity information is used to create neighborhoods around explored behaviors that cover the trajectories generated by neighboring input signals.