Provably-Correct Robot Control with LTLMoP, OMPL and ROS

This video demonstrates use of 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. The video shows a robot waiter scenario, with LTLMoP controlling both a PR2 in simulation and an Aldebaran Nao humanoid in the lab.