Unsynthesizable Cores - Minimal Explanations for Unsynthesizable High-Level Robot Behaviors
Vasumathi Raman, Hadas Kress-Gazit

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Model-Driven Software Engineering Techniques
