Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1319892,
author = {Butkova, Yuliya and Hatefi, Hassan and Hermanns, Holger and Krčál, Jan},
address = {Shanghai, China},
booktitle = {ATVA 2015},
doi = {http://dx.doi.org/10.1007/978-3-319-24953-7_12},
keywords = {Continuous time Markov decision process; time bounded reachability; uniformisation; experimental evaluation},
howpublished = {elektronická verze "online"},
language = {eng},
location = {Shanghai, China},
isbn = {978-3-319-24952-0},
pages = {166-182},
publisher = {Springer},
title = {Optimal Continuous Time Markov Decisions},
year = {2015}
}
TY - JOUR
ID - 1319892
AU - Butkova, Yuliya - Hatefi, Hassan - Hermanns, Holger - Krčál, Jan
PY - 2015
TI - Optimal Continuous Time Markov Decisions
PB - Springer
CY - Shanghai, China
SN - 9783319249520
KW - Continuous time Markov decision process
KW - time bounded reachability
KW - uniformisation
KW - experimental evaluation
N2 - In the context of Markov decision processes running in continuous time, one of the most intriguing challenges is the efficient approximation of finite horizon reachability objectives. A multitude of sophisticated model checking algorithms have been proposed for this. However, no proper benchmarking has been performed thus far. This paper presents a novel and yet simple solution: an algorithm originally developed for a restricted subclass of models and a subclass of schedulers can be twisted so as to become competitive with the more sophisticated algorithms in full generality. As the second main contribution, we perform a comparative evaluation of the core algorithmic concepts on an extensive set of benchmarks varying over all key parameters: model size, amount of non-determinism, time horizon, and precision.
ER -
BUTKOVA, Yuliya, Hassan HATEFI, Holger HERMANNS and Jan KRČÁL. Optimal Continuous Time Markov Decisions. In \textit{ATVA 2015}. Shanghai, China: Springer. p.~166-182. ISBN~978-3-319-24952-0. doi:10.1007/978-3-319-24953-7\_{}12. 2015.
|
