Optimal Control of MDPs with Temporal Logic Constraints
| Authors | |
|---|---|
| Year of publication | 2013 |
| Type | Article in Proceedings |
| Conference | Proceedings of The 52nd IEEE Conference on Decision and Control |
| MU Faculty or unit | |
| Citation | |
| Web | http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6760491 |
| Doi | http://dx.doi.org/10.1109/CDC.2013.6760491 |
| Field | Informatics |
| Keywords | automatic synthesis Markov decision processes LTL |
| Description | 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. |
| Related projects: |