Oxford logo
[KH09a] M. Kattenbelt and M. Huth. Verification and Refutation of Probabilistic Specifications via Games. In Ravi Kannan and K Narayan Kumar (editors), Proc. 29th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'09), pages 251-262, LIPIcs. December 2009. [pdf] [bib]
Downloads:  pdf pdf (288 KB)  bib bib
Abstract. We develop an abstraction-based framework to check probabilistic specifications of Markov Decision Processes (MDPs) using the stochastic two-player game abstractions (i.e. games) developed by Kwiatkowska et al. as a foundation. We define an abstraction preorder for these game abstractions which enables us to identify many new game abstractions for each MDP -- ranging from compact and imprecise to complex and precise. This added ability to trade precision for efficiency is crucial for scalable software model checking, as precise abstractions are expensive to construct in practice. Furthermore, we develop a four-valued probabilistic computation tree logic (PCTL) semantics for game abstractions. Together, the preorder and PCTL semantics comprise a powerful verification and refutation framework for arbitrary PCTL properties of MDPs.