Optimal Control of MDPs with Temporal Logic Constraints

• Autoři: SVOREŇOVÁ Mária; ČERNÁ Ivana; BELTA Calin
• Rok publikování: 2013
• Druh: Článek ve sborníku
• Konference: Proceedings of The 52nd IEEE Conference on Decision and Control
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6760491
• Doi: http://dx.doi.org/10.1109/CDC.2013.6760491
• Obor: Informatika
• Klíčová slova: automatic synthesis Markov decision processes LTL
• Popis: 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.

Související projekty

• Software Components in Embedded Systems: Development and Verification
• Řízení a ověřování vlastností komplexních hybridních systémů
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II.