Lazy Probabilistic Model Checking without Determinisation

• DOI: 10.48550/arxiv.1311.2928
• Publication Date: 2013-01-01
• Authors: Ernst Moritz Hahn; Guangyuan Li; Sven Schewe; Andrea Turrini; Lijun Zhang
• Keywords: FOS: Computer and information sciences; Computer Science - Logic in Computer Science; Formal Languages and Automata Theory (cs.FL); G.3; D.2.4; G.3; D.2.4; Computer Science - Formal Languages and Automata Theory; PLTL; 0102 computer and information sciences; 01 natural sciences; model checking; 004; Markov decision processes; Logic in Computer Science (cs.LO); determinisation; ddc:004

The bottleneck in the quantitative analysis of Markov chains and decision processes against specifications given LTL or as some form nondeterministic Büchi automata is inclusion a determinisation step automaton under consideration. In this paper, we show that full can be avoided: subset breakpoint constructions suffice. We have implemented our approach---both explicit symbolic versions---in prototype tool. Our experiments compete with mature tools like PRISM.