Automated feedback for unachievable high-level robot behaviors

One of the main challenges in robotics is the generation of controllers for autonomous, high-level robot behaviors comprising a non-trivial sequence of actions. Recently, formal methods have emerged as a powerful tool for automatically generating autonomous robot controllers that guarantee desired behaviors expressed by a class of temporal logic specifications. However, when there is no controller that fulfills the specification, these approaches do not provide the user with a source of failure, making the troubleshooting of specifications an unstructured and time-consuming process. In this paper, we describe a procedure for analyzing an unsynthesizable specification to identify causes of failure. We also provide an interactive game for exploring possible causes of failure, in which the user attempts to fulfill the robot specification against an adversarial environment. Our approach is implemented within the LTLMoP toolkit for robot mission planning.