Hahn, Ernst Moritz; Li, Guangyuan; Schewe, Sven; Turrini, Andrea; Zhang, Lijun Lazy probabilistic model checking without determinisation. (English) Zbl 1374.68290 Aceto, Luca (ed.) et al., 26th international conference on concurrency theory, CONCUR’15, Madrid, Spain, September 1–4, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-91-0). LIPIcs – Leibniz International Proceedings in Informatics 42, 354-367 (2015). Summary: 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.For the entire collection see [Zbl 1329.68017]. Cited in 13 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 68Q45 Formal languages and automata 68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) Keywords:Markov decision processes; model checking; PLTL; determinisation; nondeterministic automata PDFBibTeX XMLCite \textit{E. M. Hahn} et al., LIPIcs -- Leibniz Int. Proc. Inform. 42, 354--367 (2015; Zbl 1374.68290) Full Text: DOI arXiv