Receding horizon surveillance with temporal logic specifications

In this paper we consider a setting where a robotic vehicle is commissioned to provide surveillance in an area where there are multiple targets, while satisfying a set of high level, rich specifications expressed as Linear Temporal Logic formulas. Each target has an associated reward. The goal of the vehicle is to maximize the cumulative collected reward while satisfying the given high level task specification. By the nature of a surveillance mission, targets points of interest are detected in real time around the current location of the vehicle; hence we employ a receding horizon controller to compute the optimal path of the vehicle inside a subset of the mission space. This paper provides a framework which guarantees that the overall trajectory of the system satisfies the desired linear temporal logic specification, while the control decisions are made based on local information obtained in real time.