Oxford logo
[KH09] M. Kattenbelt and M. Huth. Abstraction Framework for Markov Decision Processes and PCTL Via Games. Technical report RR-09-01, Oxford University Computing Laboratory. March 2009. [pdf]
Downloads:  pdf pdf (517 KB)
Abstract. Markov decision processes (MDPs) are natural models of computation in a wide range of applications. Probabilistic computation tree logic (PCTL) is a powerful temporal logic for reasoning about and verifying such models. Often, these models are prohibitively large or infinite-state, and so direct model checking of PCTL formulae over MDPs is infeasible. A recognised solution to this problem would be to develop finite-state abstractions of MDPs that soundly abstract the satisfaction of arbitrary PCTL formulae over very large or infinite-state MDPs. We state requirements for such an abstraction framework -- e.g. that model checking of abstractions under-approximates generalised model checking for PCTL -- and show important meta-properties that follow from these requirements. We take a notion of stochastic games from stochastic reachability analysis, adapt it, develop a simulation order for these adapted games -- decidable in PTIME -- and prove that this adaptation meets all key requirements for an abstraction framework. Unlike generalised model checking, model checking our abstractions is reasonably efficient. We also show that the refinement characterised by PCTL is coarser than our simulation order.