×

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].

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.)
PDFBibTeX XMLCite
Full Text: DOI arXiv