@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}
}

{"_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"]}