LTL Planning in Dynamic Environments

This paper addresses the path planning problem of a mobile robot based on linear temporal logic formulae over a set of regions of interest in the environment. The regions have fixed and known locations but have some dynamic observations that can appear and disappear based on exponential probability density functions. The robot movement capabilities are modeled by a finite-state transition system. By drawing inspiration from temporal logic control for static environments, we find a run that has the greatest chance of satisfying the temporal logic specification. Then, we devise a supervising strategy for the robot motion along this run, which updates the execution based on the currently observed regions. The approach is supported by two simulations.