Explaining Impossible High-Level Robot Behaviors

A key challenge in robotics is the generation of controllers for autonomous, high-level robot behaviors comprising nontrivial sequences of actions, including reactive and repeated tasks. When constructing controllers to fulfill such tasks, it is often not known a priori whether the intended behavior is even feasible; plans are modified on the fly to deal with failures that occur during execution, often still without guaranteeing correct behavior. Recently, formal methods have emerged as a powerful tool to automatically generate autonomous robot controllers that guarantee desired behaviors expressed by a class of temporal logic specifications. However, when the specification cannot be fulfilled, these approaches do not provide the user with a source of failure, making the troubleshooting of specifications an unstructured and time-consuming process. This paper describes an algorithm to automatically analyze an unsynthesizable specification in order to identify causes of failure. It also introduces an interactive game to explore possible causes of unsynthesizability, in which the user attempts to fulfill the robot specification against an adversarial environment. The proposed algorithm and game are implemented as features within the LTLMoP toolkit for robot mission planning.