Unsynthesizable Cores - Minimal Explanations for Unsynthesizable High-Level Robot Behaviors

Abstract

With the increasing ubiquity of multi-capable, general-purpose robots arises the need for enabling non-expert users to command these robots to perform complex high-level tasks. To this end, high-level robot control has seen the application of formal methods to automatically synthesize correct-by-construction controllers from user-defined specifications; synthesis fails if and only if there exists no controller that achieves the specified behavior. Recent work has also addressed the challenge of providing easy-to-understand feedback to users when a specification fails to yield a corresponding controller. Existing techniques provide feedback on portions of the specification that cause the failure, but do so at a coarse granularity. This work presents techniques for refining this feedback, extracting minimal explanations of unsynthesizability.