BDD for Complete Characterization of a Safety Violation in Linear Systems with Inputs

The control design tools for linear systems typically involves pole placement and computing Lyapunov functions which are useful for ensuring stability. But given higher requirements on control design, a designer is expected to satisfy other specification such as safety or temporal logic specification as well, and a naive control design might not satisfy such specification. A control designer can employ model checking as a tool for checking safety and obtain a counterexample in case of a safety violation. While several scalable techniques for verification have been developed for safety verification of linear dynamical systems, such tools merely act as decision procedures to evaluate system safety and, consequently, yield a counterexample as an evidence to safety violation. However these model checking methods are not geared towards discovering corner cases or re-using verification artifacts for another sub-optimal safety specification. In this paper, we describe a technique for obtaining complete characterization of counterexamples for a safety violation in linear systems. The proposed technique uses the reachable set computed during safety verification for a given temporal logic formula, performs constraint propagation, and represents all modalities of counterexamples using a binary decision diagram (BDD). We introduce an approach to dynamically determine isomorphic nodes for obtaining a considerably reduced (in size) decision diagram. A thorough experimental evaluation on various benchmarks exhibits that the reduction technique achieves up to $67\%$ reduction in the number of nodes and $75\%$ reduction in the width of the decision diagram.

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 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.

Safety and progress proofs for a reactive planner and controller for autonomous driving

In this paper, we perform safety and performance analysis of an autonomous vehicle that implements reactive planner and controller for navigating a race lap. Unlike traditional planning algorithms that have access to a map of the environment, reactive planner generates the plan purely based on the current input from sensors. Our reactive planner selects a waypoint on the local Voronoi diagram and we use a pure-pursuit controller to navigate towards the waypoint. Our safety and performance analysis has two parts. The first part demonstrates that the reactive planner computes a plan that is locally consistent with the Voronoi plan computed with full map. The second part involves modeling of the evolution of vehicle navigating along the Voronoi diagram as a hybrid automata. For proving the safety and performance specification, we compute the reachable set of this hybrid automata and employ some enhancements that make this computation easier. We demonstrate that an autonomous vehicle implementing our reactive planner and controller is safe and successfully completes a lap for five different circuits. In addition, we have implemented our planner and controller in a simulation environment as well as a scaled down autonomous vehicle and demonstrate that our planner works well for a wide variety of circuits.