| BRÁZDIL, Tomáš, Chatterjee KRISHNENDU, Vojtěch FOREJT and 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, p. 181-187. ISBN 978-3-662-46680-3. Available from: https://dx.doi.org/10.1007/978-3-662-46681-0_12. |
Other formats:
BibTeX
LaTeX
RIS
@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 and 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, p.~181-187. ISBN~978-3-662-46680-3. Available from: https://dx.doi.org/10.1007/978-3-662-46681-0\_{}12.
|
