  We present a method to find an optimal policy with respect to a reward
function for a discounted Markov decision process under general linear temporal
logic (LTL) specifications. Previous work has either focused on maximizing a
cumulative reward objective under finite-duration tasks, specified by
syntactically co-safe LTL, or maximizing an average reward for persistent
(e.g., surveillance) tasks. This paper extends and generalizes these results by
introducing a pair of occupancy measures to express the LTL satisfaction
objective and the expected discounted reward objective, respectively. These
occupancy measures are then connected to a single policy via a novel reduction
resulting in a mixed integer linear program whose solution provides an optimal
policy. Our formulation can also be extended to include additional constraints
with respect to secondary reward functions. We illustrate the effectiveness of
our approach in the context of robotic motion planning for complex missions
under uncertainty and performance objectives.
