D
2013
Optimal Control of MDPs with Temporal Logic Constraints
SVOREŇOVÁ, Mária, Ivana ČERNÁ a Calin BELTA
Základní údaje
Originální název
Optimal Control of MDPs with Temporal Logic Constraints
Autoři
SVOREŇOVÁ, Mária (703 Slovensko, domácí),
Ivana ČERNÁ (203 Česká republika, garant, domácí) a Calin BELTA (840 Spojené státy)
Vydání
Neuveden, Proceedings of The 52nd IEEE Conference on Decision and Control, od s. 3938-3943, 6 s. 2013
Nakladatel
Omnipress for the IEEE Control Systems Society
Další údaje
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Česká republika
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
elektronická verze "online"
Kód RIV
RIV/00216224:14330/13:00066298
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
automatic synthesis Markov decision processes LTL
Příznaky
Mezinárodní význam, Recenzováno
V originále
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.
Návaznosti
GAP202/11/0312, projekt VaV | Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems) | Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification |
|
LH11065, projekt VaV | Název: Řízení a ověřování vlastností komplexních hybridních systémů (Akronym: Řízení a ověřování vlastností komplexních hybridní) | Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Řízení a ověřování vlastností komplexních hybridních systémů |
|
MUNI/A/0760/2012, interní kód MU | Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.) | Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty |
|
Zobrazeno: 21. 10. 2024 01:20