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

TL;DR

This paper introduces methods for generating minimal explanations for why certain high-level robot behavior specifications cannot be automatically synthesized, improving user feedback clarity.

Contribution

It proposes novel techniques to refine feedback on unsynthesizable specifications, providing minimal explanations that clarify the causes of synthesis failure.

Findings

Effective extraction of minimal unsynthesizability explanations

Improved user understanding of specification failures

Enhanced feedback granularity over existing methods

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.