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.

Dynamic Selection of Perception Models for Robotic Control

Robotic perception models, such as Deep Neural Networks (DNNs), are becoming more computationally intensive and there are several models being trained with accuracy and latency trade-offs. However, modern latency accuracy trade-offs largely report mean accuracy for single-step vision tasks, but there is little work showing which model to invoke for multi-step control tasks in robotics. The key challenge in a multi-step decision making is to make use of the right models at right times to accomplish the given task. That is, the accomplishment of the task with a minimum control cost and minimum perception time is a desideratum; this is known as the model selection problem. In this work, we precisely address this problem of invoking the correct sequence of perception models for multi-step control. In other words, we provide a provably optimal solution to the model selection problem by casting it as a multi-objective optimization problem balancing the control cost and perception time. The key insight obtained from our solution is how the variance of the perception models matters (not just the mean accuracy) for multi-step decision making, and to show how to use diverse perception models as a primitive for energy-efficient robotics. Further, we demonstrate our approach on a photo-realistic drone landing simulation using visual navigation in AirSim. Using our proposed policy, we achieved 38.04% lower control cost with 79.1% less perception time than other competing benchmarks.

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.

Interpretable Trade-offs Between Robot Task Accuracy and Compute Efficiency

A robot can invoke heterogeneous computation resources such as CPUs, cloud GPU servers, or even human computation for achieving a high-level goal. The problem of invoking an appropriate computation model so that it will successfully complete a task while keeping its compute and energy costs within a budget is called a model selection problem. In this paper, we present an optimal solution to the model selection problem with two compute models, the first being fast but less accurate, and the second being slow but more accurate. The main insight behind our solution is that a robot should invoke the slower compute model only when the benefits from the gain in accuracy outweigh the computational costs. We show that such cost-benefit analysis can be performed by leveraging the statistical correlation between the accuracy of fast and slow compute models. We demonstrate the broad applicability of our approach to diverse problems such as perception using neural networks and safe navigation of a simulated Mars rover.

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.