Provably-correct robot control with LTLMoP, OMPL and ROS

This paper illustrates the Linear Temporal Logic MissiOn Planning (LTLMoP) toolkit. LTLMoP is an open source software package that transforms high-level specifications for robot behavior, captured using a structured English grammar, into a robot controller that guarantees the robot will complete its task, if the task is feasible. If the task cannot be guaranteed, LTLMoP provides feedback to the user as to what the problem is. Due to its modular nature, users can control a variety of different robots using LTLMoP, both simulated and physical, with the same specification. It shows an example robot waiter scenario, with LTLMoP controlling both a PR2 in simulation (using Gazebo), showcasing the interface between LTLMoP and the Robot Operating System (ROS)2, as well as an Aldebaran Nao humanoid in the lab.