# Optimal Control of MDPs with Temporal Logic Constraints

arXiv: https://arxiv.org/abs/1303.1942 · HTML: https://mlsanity.com/paper/1303.1942/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Mar 2013.

## Built on by (most cited first, 1 of 1)

- [Controller Synthesis for Omega-Regular and Steady-State Specifications](https://mlsanity.com/paper/2106.02951/) (2021)

## Abstract (arXiv)

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.