SVOREŇOVÁ, Mária, Ivana ČERNÁ and Calin BELTA. Optimal Control of MDPs with Temporal Logic Constraints. In Proceedings of The 52nd IEEE Conference on Decision and Control. Neuveden: Omnipress for the IEEE Control Systems Society. p. 3938-3943. ISBN 978-1-4673-5714-2. doi:10.1109/CDC.2013.6760491. 2013.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Optimal Control of MDPs with Temporal Logic Constraints
Authors SVOREŇOVÁ, Mária (703 Slovakia, belonging to the institution), Ivana ČERNÁ (203 Czech Republic, guarantor, belonging to the institution) and Calin BELTA (840 United States of America).
Edition Neuveden, Proceedings of The 52nd IEEE Conference on Decision and Control, p. 3938-3943, 6 pp. 2013.
Publisher Omnipress for the IEEE Control Systems Society
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Czech Republic
Confidentiality degree is not subject to a state or trade secret
Publication form electronic version available online
WWW URL
RIV identification code RIV/00216224:14330/13:00066298
Organization unit Faculty of Informatics
ISBN 978-1-4673-5714-2
ISSN 0743-1546
Doi http://dx.doi.org/10.1109/CDC.2013.6760491
UT WoS 000352223504076
Keywords in English automatic synthesis Markov decision processes LTL
Tags core_A, firank_A
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 31/3/2014 12:52.
Abstract
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.
Links
GAP202/11/0312, research and development projectName: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)
Investor: Czech Science Foundation
LH11065, research and development projectName: Řízení a ověřování vlastností komplexních hybridních systémů (Acronym: Řízení a ověřování vlastností komplexních hybridní)
Investor: Ministry of Education, Youth and Sports of the CR
MUNI/A/0760/2012, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)
Investor: Masaryk University, Category A
PrintDisplayed: 28/3/2024 18:28