Towards minimal explanations of unsynthesizability for high-level robot behaviors

Abstract

High-level robot control has recently seen the application of formal methods to the automatic synthesis of correct-by-construction controllers from user-defined specifications. When a specification fails to yield a corresponding controller, existing techniques provide feedback on portions of the specification that cause the failure, but at a coarse granularity. This work provides techniques for extracting minimal explanations of such failures. The approach is shown to provide refinement of the feedback on several example specifications.