One of the main challenges in robotics is the gener- ation 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 specifica- tions. 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.
Mendeley saves you time finding and organizing research
Choose a citation style from the tabs below