Optimal Continuous Time Markov Decisions. Butkova, Y., Hatefi, H., Hermanns, H., & Krcál, J. In Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, 2015. abstract bibtex 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.
@inProceedings{
title = {Optimal Continuous Time Markov Decisions},
type = {inProceedings},
year = {2015},
id = {f63cbd26-7ae7-3e2a-b85b-335f74015587},
created = {2015-07-05T19:44:15.000Z},
file_attached = {false},
profile_id = {4f325e21-a764-32ab-9623-e568e98285be},
last_modified = {2017-03-25T21:52:16.230Z},
read = {false},
starred = {false},
authored = {true},
confirmed = {true},
hidden = {false},
citation_key = {ButkovaHHK15},
source_type = {inproceedings},
notes = {to appear},
private_publication = {false},
abstract = { 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. },
bibtype = {inProceedings},
author = {Butkova, Yuliya and Hatefi, Hassan and Hermanns, Holger and Krcál, Jan},
booktitle = {Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015}
}
Downloads: 0
{"_id":"y4wMa55v3WZaC2hZx","bibbaseid":"butkova-hatefi-hermanns-krcl-optimalcontinuoustimemarkovdecisions-2015","downloads":0,"creationDate":"2015-07-05T19:45:41.023Z","title":"Optimal Continuous Time Markov Decisions","author_short":["Butkova, Y.","Hatefi, H.","Hermanns, H.","Krcál, J."],"year":2015,"bibtype":"inProceedings","biburl":null,"bibdata":{"title":"Optimal Continuous Time Markov Decisions","type":"inProceedings","year":"2015","id":"f63cbd26-7ae7-3e2a-b85b-335f74015587","created":"2015-07-05T19:44:15.000Z","file_attached":false,"profile_id":"4f325e21-a764-32ab-9623-e568e98285be","last_modified":"2017-03-25T21:52:16.230Z","read":false,"starred":false,"authored":"true","confirmed":"true","hidden":false,"citation_key":"ButkovaHHK15","source_type":"inproceedings","notes":"to appear","private_publication":false,"abstract":" In the context of Markov decision processes running in\ncontinuous time, one of the most intriguing\nchallenges is the efficient approximation of finite\nhorizon reachability objectives. A multitude of\nsophisticated model checking algorithms have been\nproposed for this. However, no proper benchmarking\nhas been performed thus far. This paper presents a\nnovel and yet simple solution: an algorithm\noriginally developed for a restricted subclass of\nmodels and a subclass of schedulers can be twisted\nso as to become competitive with the more\nsophisticated algorithms in full generality. As the\nsecond main contribution, we perform a comparative\nevaluation of the core algorithmic concepts on an\nextensive set of benchmarks varying over all key\nparameters: model size, amount of non-determinism,\ntime horizon, and precision. ","bibtype":"inProceedings","author":"Butkova, Yuliya and Hatefi, Hassan and Hermanns, Holger and Krcál, Jan","booktitle":"Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015","bibtex":"@inProceedings{\n title = {Optimal Continuous Time Markov Decisions},\n type = {inProceedings},\n year = {2015},\n id = {f63cbd26-7ae7-3e2a-b85b-335f74015587},\n created = {2015-07-05T19:44:15.000Z},\n file_attached = {false},\n profile_id = {4f325e21-a764-32ab-9623-e568e98285be},\n last_modified = {2017-03-25T21:52:16.230Z},\n read = {false},\n starred = {false},\n authored = {true},\n confirmed = {true},\n hidden = {false},\n citation_key = {ButkovaHHK15},\n source_type = {inproceedings},\n notes = {to appear},\n private_publication = {false},\n abstract = { In the context of Markov decision processes running in\ncontinuous time, one of the most intriguing\nchallenges is the efficient approximation of finite\nhorizon reachability objectives. A multitude of\nsophisticated model checking algorithms have been\nproposed for this. However, no proper benchmarking\nhas been performed thus far. This paper presents a\nnovel and yet simple solution: an algorithm\noriginally developed for a restricted subclass of\nmodels and a subclass of schedulers can be twisted\nso as to become competitive with the more\nsophisticated algorithms in full generality. As the\nsecond main contribution, we perform a comparative\nevaluation of the core algorithmic concepts on an\nextensive set of benchmarks varying over all key\nparameters: model size, amount of non-determinism,\ntime horizon, and precision. },\n bibtype = {inProceedings},\n author = {Butkova, Yuliya and Hatefi, Hassan and Hermanns, Holger and Krcál, Jan},\n booktitle = {Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015}\n}","author_short":["Butkova, Y.","Hatefi, H.","Hermanns, H.","Krcál, J."],"bibbaseid":"butkova-hatefi-hermanns-krcl-optimalcontinuoustimemarkovdecisions-2015","role":"author","urls":{},"downloads":0},"search_terms":["optimal","continuous","time","markov","decisions","butkova","hatefi","hermanns","krcál"],"keywords":[],"authorIDs":["5457d87e2abc8e9f370007e5","54d6986996f9453b5f00073b"]}