MultiGain: A Controller Synthesis Tool for MDPs with Multiple
Mean-Payoff Objectives

D 2015

MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives

BRÁZDIL, Tomáš, Chatterjee KRISHNENDU, Vojtěch FOREJT a Antonín KUČERA

Základní údaje

Originální název

MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives

Autoři

BRÁZDIL, Tomáš (203 Česká republika, domácí), Chatterjee KRISHNENDU (40 Rakousko), Vojtěch FOREJT (203 Česká republika) a Antonín KUČERA (203 Česká republika, garant, domácí)

Vydání

Heidelberg, Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. od s. 181-187, 7 s. 2015

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/15:00081426

Organizační jednotka

Fakulta informatiky

ISBN

978-3-662-46680-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-662-46681-0_12

Klíčová slova anglicky

Markov decision processes; mean-payoff reward; multi-objective optimisation; formal verification

Štítky

core_A, firank_A, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 4. 2016 15:34, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i) generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii) generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies.

Návaznosti

GBP202/12/G061, projekt VaV

Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

Citovat

BRÁZDIL, Tomáš, Chatterjee KRISHNENDU, Vojtěch FOREJT a Antonín KUČERA. MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives. In Christel Baier, Cesare Tinelli. Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Heidelberg: Springer, 2015, s. 181-187. ISBN 978-3-662-46680-3. Dostupné z: https://dx.doi.org/10.1007/978-3-662-46681-0_12.

@inproceedings{1323105,
   author = {Brázdil, Tomáš and Krishnendu, Chatterjee and Forejt, Vojtěch and Kučera, Antonín},
   address = {Heidelberg},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings.},
   doi = {http://dx.doi.org/10.1007/978-3-662-46681-0_12},
   editor = {Christel Baier, Cesare Tinelli},
   keywords = {Markov decision processes; mean-payoff reward; multi-objective optimisation; formal verification},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Heidelberg},
   isbn = {978-3-662-46680-3},
   pages = {181-187},
   publisher = {Springer},
   title = {MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives},
   year = {2015}
}

TY  - JOUR
ID  - 1323105
AU  - Brázdil, Tomáš - Krishnendu, Chatterjee - Forejt, Vojtěch - Kučera, Antonín
PY  - 2015
TI  - MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives
PB  - Springer
CY  - Heidelberg
SN  - 9783662466803
KW  - Markov decision processes
KW  - mean-payoff reward
KW  - multi-objective optimisation
KW  - formal verification
N2  - We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i) generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii) generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies.
ER  -

BRÁZDIL, Tomáš, Chatterjee KRISHNENDU, Vojtěch FOREJT a Antonín KUČERA. MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives. In Christel Baier, Cesare Tinelli. \textit{Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings.}. Heidelberg: Springer, 2015, s.~181-187. ISBN~978-3-662-46680-3. Dostupné z: https://dx.doi.org/10.1007/978-3-662-46681-0\_{}12.

Podrobný výpis o publikaci