Lazy Probabilistic Model Checking without Determinisation

26^th April 2016, 13:00 Ashton Lecture Theater
Dr. Ernst Moritz Hahn
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences.
Room A219, Building 5
Telephone: +86 10-62661604
Address: South Fourth Street 4#, Zhong Guan Cun

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 talk, 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.