Optimal Control of MDPs with Temporal Logic Constraints

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

Jazyk

angličtina

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"

Odkazy

URL

Kód RIV

RIV/00216224:14330/13:00066298

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4673-5714-2

ISSN

DOI

http://dx.doi.org/10.1109/CDC.2013.6760491

UT WoS

000352223504076

Klíčová slova anglicky

automatic synthesis Markov decision processes LTL

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 31. 3. 2014 12:52, prof. RNDr. Ivana Černá, CSc.

Anotace

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

Citovat

SVOREŇOVÁ, Mária, Ivana ČERNÁ a Calin BELTA. Optimal Control of MDPs with Temporal Logic Constraints. Online. In Proceedings of The 52nd IEEE Conference on Decision and Control. Neuveden: Omnipress for the IEEE Control Systems Society, 2013, s. 3938-3943. ISBN 978-1-4673-5714-2. Dostupné z: https://dx.doi.org/10.1109/CDC.2013.6760491.

@inproceedings{1120956,
   author = {Svoreňová, Mária and Černá, Ivana and Belta, Calin},
   address = {Neuveden},
   booktitle = {Proceedings of The 52nd IEEE Conference on Decision and Control},
   doi = {http://dx.doi.org/10.1109/CDC.2013.6760491},
   keywords = {automatic synthesis Markov decision processes LTL},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-1-4673-5714-2},
   pages = {3938-3943},
   publisher = {Omnipress for the IEEE Control Systems Society},
   title = {Optimal Control of MDPs with Temporal Logic Constraints},
   url = {http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6760491},
   year = {2013}
}

TY  - JOUR
ID  - 1120956
AU  - Svoreňová, Mária - Černá, Ivana - Belta, Calin
PY  - 2013
TI  - Optimal Control of MDPs with Temporal Logic Constraints
PB  - Omnipress for the IEEE Control Systems Society
CY  - Neuveden
SN  - 9781467357142
KW  - automatic synthesis Markov decision processes LTL
UR  - http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6760491
N2  - 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.
ER  -

SVOREŇOVÁ, Mária, Ivana ČERNÁ a Calin BELTA. Optimal Control of MDPs with Temporal Logic Constraints. Online. In \textit{Proceedings of The 52nd IEEE Conference on Decision and Control}. Neuveden: Omnipress for the IEEE Control Systems Society, 2013, s.~3938-3943. ISBN~978-1-4673-5714-2. Dostupné z: https://dx.doi.org/10.1109/CDC.2013.6760491.

Podrobný výpis o publikaci