Optimal Control of MDPs with Temporal Logic Constraints

Investor logo

Warning

This publication doesn't include Institute of Computer Science. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

SVOREŇOVÁ Mária ČERNÁ Ivana BELTA Calin

Year of publication 2013
Type Article in Proceedings
Conference Proceedings of The 52nd IEEE Conference on Decision and Control
MU Faculty or unit

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.

More info