Optimal and Dynamic Planning for Markov Decision Processes with Co-Safe LTL Specifications

We present a method to specify tasks and synthesise cost-optimal policies for Markov decision processes using co-safe linear temporal logic. Our approach incorporates a dynamic task handling procedure which allows for the addition of new tasks during execution and provides the ability to replan an optimal policy on-the-fly. This new policy minimises the cost to satisfy the conjunction of the current tasks and the new one, taking into account how much of the current tasks has already been executed. We illustrate our approach by applying it to motion planning for a mobile service robot.