Unsynthesizable Cores - Minimal Explanations for Unsynthesizable High-Level Robot Behaviors
This work addresses the need for non-expert users to understand why their commands fail in high-level robot control, offering incremental improvements over existing coarse-grained feedback methods.
The paper tackles the problem of providing detailed feedback when robot behavior specifications are unsynthesizable, presenting techniques to extract minimal explanations for synthesis failures.
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.