In this paper, we focus on formal synthesis of control policies for finite Markov decision processes with non-negative real-valued costs. We develop an algorithm to automatically generate a policy that guarantees the satisfaction of a correctness specification expressed as a formula of Linear Temporal Logic, while at the same time minimizing the expected average cost between two consecutive satisfactions of a desired property. The existing solutions to this problem are sub-optimal. By leveraging ideas from automata-based model checking and game theory, we provide an optimal solution. We demonstrate the approach on an illustrative example.
@article{arxiv.1303.1942,
title = {Optimal Control of MDPs with Temporal Logic Constraints},
author = {Maria Svorenova and Ivana Cerna and Calin Belta},
journal= {arXiv preprint arXiv:1303.1942},
year = {2013}
}