[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]
|
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.
|