A GUI Design of Robot Motion and Task Planning Based on Linear Temporal Logic

Abstract: Recent approaches solve the problem of robot motion and task planning by using formal methods-based model checking algorithms. In this work, we consider the software package P-MAS-TG, an automatic tool to generate correct-by-design controllers for robot motion and task planning. The robot motion can be modelled as a finite-state transition system and the task can be represented by a linear temporal logic formula. Then, using a model checking algorithm, an accepting path for the robot motion can be found so that the robot satisfies the specific linear temporal logic task. In this thesis, the process of searching for the accepting path of the robot motion by P-MAS-TG is visualized by means of a graphical user interface (GUI) in form of an rqt plug-in where all requested inputs for the P-MAS-TG package can be defined in the GUI so that the process is simplified and user-friendly. Moreover, the GUI provides a simple hybrid control mechanism between the initial linear temporal logic task and a temporary task that is inserted by a human.
All functions of the GUI are implemented and demonstrated on the TurtleBot platform. The experiment shows that the GUI and the P-MAS-TG are successfully integrated. Features of the P-MAS-TG are performed with the GUI to conduct motion planning and task planning on the TurtleBot.

Examiner: Dimos Dimarogonas