Optimal Control of MDPs with Temporal Logic Constraints

D 2013

Optimal Control of MDPs with Temporal Logic Constraints

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

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

References:

URL

RIV identification code

RIV/00216224:14330/13:00066298

Organization unit

Faculty of Informatics

ISBN

978-1-4673-5714-2

ISSN

DOI

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

UT WoS

000352223504076

Keywords in English

automatic synthesis Markov decision processes LTL

Abstract

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.

Links

GAP202/11/0312, research and development project

Name: 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 project

Name: Ří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 MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)

Investor: Masaryk University, Category A

Citovat

SVOREŇOVÁ, Mária, Ivana ČERNÁ and 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, p. 3938-3943. ISBN 978-1-4673-5714-2. Available from: 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Á and 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, p.~3938-3943. ISBN~978-1-4673-5714-2. Available from: https://dx.doi.org/10.1109/CDC.2013.6760491.

Detailed Information on Publication Record