In this paper, we perform a safety and performance analysis of an autonomous vehicle utilizing a reactive planner and controller to navigate a race lap. Unlike traditional planning algorithms that use a map of the environment, the reactive planner generates the plan based solely on current sensor inputs. Our reactive planner selects a waypoint on the local Voronoi diagram, and we use a pure-pursuit controller to navigate towards this waypoint.Our analysis consists of two parts. The first part demonstrates that the reactive planner computes a plan locally consistent with the Voronoi plan derived from a full map. The second part models the vehicle’s navigation along the Voronoi diagram as a hybrid automaton. To prove the safety and performance specifications, we compute the reachable set of this hybrid automaton and apply enhancements to simplify this computation. We show that an autonomous vehicle using our reactive planner and controller is safe and successfully completes a lap on five different circuits. Additionally, we have implemented our planner and controller in a simulation environment and on a scaled-down autonomous vehicle, demonstrating that our approach works well across a variety of circuits.

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.