Temporal logic robot mission planning for slow and fast actions

This paper addresses the challenge of creating correct-by-construction controllers for robots whose actions are of varying execution durations. Recently, Linear Temporal Logic synthesis has been used to construct robot controllers for performing high-level tasks. During continuous execution of these controllers by a physical robot, one or more low-level controllers are invoked simultaneously. If these low-level behaviors take different lengths of time to complete, the system will pass through several potentially unsafe intermediate states. This paper presents an algorithm that either generates a hybrid controller such that every continuous behavior of the robot is safe, or determines at synthesis time that the behavior may be unsafe. The proposed approach is implemented within the LTLMoP toolkit for reactive mission planning.