Lazy Probabilistic Model Checking without Determinisation
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\"uchi 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.
Keywords
Cite
@article{arxiv.1311.2928,
title = {Lazy Probabilistic Model Checking without Determinisation},
author = {Ernst Moritz Hahn and Guangyuan Li and Sven Schewe and Andrea Turrini and Lijun Zhang},
journal= {arXiv preprint arXiv:1311.2928},
year = {2015}
}
Comments
38 pages. Updated version for introducing the following changes: - general improvement on paper presentation; - extension of the approach to avoid full determinisation; - added proofs for such an extension; - added case studies; - updated old case studies to reflect the added extension