Minimal Explanations for Impossible High-Level Robot Behaviors

A key challenge in robotics is the automated construction of controllers for high-level tasks, including reactive behaviors and repeated goals. Recently, Linear Temporal Logic synthesis has emerged as a powerful tool for generating hybrid controllers that guarantee desired behaviors expressed by temporal logic specifications. Most approaches use a discrete abstraction of the robot workspace and a logic specification of the environment assumptions and desired robot behavior; the synthesized controllers are provably correct with respect to this abstraction and specification.

However, when there does not exist a controller that fulfills a given specification, troubleshooting can be an unstructured and time-consuming process. This talk will present results on automating the analysis of such "unsynthesizable" specifications. It will discuss the distinct types of failure that can occur, and identify techniques for distinguishing them. Additionally, it will present an approach to identifying minimal sources of failure, based on unsatisfiable cores of propositional SAT encodings of the specification and the adversarial environment.

This is joint work with Cameron Finucane and Hadas Kress-Gazit.

Vasu Raman is a Computing and Mathematical Sciences postdoctoral scholar at the California Institute of Technology, Pasadena, CA. Her current research interests lie at the intersection of autonomous high-level control and formal methods, with applications in robotics and the control of cyber-physical systems. Previous projects have included analyzing specifications that are impossible from a formal synthesis standpoint, and bridging the gap between provably correct discrete solutions and their continuous implementations. She earned a PhD in Computer Science in 2013 from Cornell University, NY, where she was advised by Hadas Kress-Gazit. She also holds a BA in Computer Science and Mathematics from Wellesley College, MA.