Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2015.354
URN: urn:nbn:de:0030-drops-53918
URL: https://drops.dagstuhl.de/opus/volltexte/2015/5391/
Hahn, Ernst Moritz ; Li, Guangyuan ; Schewe, Sven ; Turrini, Andrea ; Zhang, Lijun
Lazy Probabilistic Model Checking without Determinisation
| pdf-format: |
|
Abstract
The bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Büchi automata is the inclusion of a determinisation step of the automaton under consideration. In this paper, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approach - both explicit and symbolic versions - in a prototype tool. Our experiments show that our prototype can compete with mature tools like PRISM.
BibTeX - Entry
@InProceedings{hahn_et_al:LIPIcs:2015:5391,
author = {Ernst Moritz Hahn and Guangyuan Li and Sven Schewe and Andrea Turrini and Lijun Zhang},
title = {{Lazy Probabilistic Model Checking without Determinisation}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {354--367},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-91-0},
ISSN = {1868-8969},
year = {2015},
volume = {42},
editor = {Luca Aceto and David de Frutos Escrig},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5391},
URN = {urn:nbn:de:0030-drops-53918},
doi = {10.4230/LIPIcs.CONCUR.2015.354},
annote = {Keywords: Markov decision processes, model checking, PLTL, determinisation}
}
| Keywords: | Markov decision processes, model checking, PLTL, determinisation | |
| Seminar: | 26th International Conference on Concurrency Theory (CONCUR 2015) | |
| Issue date: | 2015 | |
| Date of publication: | 26.08.2015 |
