[HahnLSTZ15] Lazy Probabilistic Model Checking without Determinisation Hahn, E. M.; Li, G.; Schewe, S.; Turrini, A. and Zhang, L. In CONCUR, pages 354-367, LIPIcs 42, 2015.
Downloads: pdf, bibURL: 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