Optimal Continuous Time Markov Decisions
| Autoři | |
|---|---|
| Rok publikování | 2015 |
| Druh | Článek ve sborníku |
| Konference | ATVA 2015 |
| Fakulta / Pracoviště MU | |
| Citace | |
| Doi | http://dx.doi.org/10.1007/978-3-319-24953-7_12 |
| Obor | Informatika |
| Klíčová slova | Continuous time Markov decision process; time bounded reachability; uniformisation; experimental evaluation |
| Popis | 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. |
| Související projekty: |