@inproceedings{KH09,
  author = "M. Kattenbelt and M. Huth",
  booktitle = "Proc. 29th International Conference on the Foundations of Software Technology and Theoretical Computer Science (FSTTCS `09)",
  howpublished = "To appear",
  title = "Verification and Refutation of Probabilistic Specifications via Games",
  year = "2009",
}


    
      @techreport{RR-09-01,
  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 underapproximates generalised model checking for PCTL ? and show important metaproperties 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 P ? 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.",
  author = "Mark Kattenbelt and Michael Huth",
  institution = "Oxford University Computing Laboratory",
  number = "RR-09-01",
  pages = "45",
  title = "Abstraction Framework for Markov Decision Processes and PCTL via Games",
  url = "http://qav.comlab.ox.ac.uk/papers/KH09.pdf",
  year = "2009",
}


    
      @inproceedings{KKNP09,
  author = "M. Kattenbelt, M. Kwiatkowska, G. Norman and D. Parker",
  booktitle = "Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI `09)",
  month = "January",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  title = "Abstraction Refinement for Probabilistic Software",
  url = "http://qav.comlab.ox.ac.uk/papers/vmcai09.pdf",
  year = "2009",
}


    
      @inproceedings{KKNP08a,
  author = "M. Kattenbelt and M. Kwiatkowska and G. Norman and D. Parker",
  booktitle = "Proc. 6th Workshop on Quantitative Aspects of Programming Languages (QAPL'08)",
  title = "Game-Based Probabilistic Predicate Abstraction in {PRISM}",
  url = "http://qav.comlab.ox.ac.uk/papers/qapl08.pdf",
  year = "2008",
}


    
      @techreport{KKNP08b,
  author = "M. Kattenbelt and M. Kwiatkowska and G. Norman and D. Parker",
  institution = "Oxford University Computing Laboratory",
  month = "February",
  number = "RR-08-01",
  title = "Game-Based Probabilistic Predicate Abstraction in {PRISM}",
  url = "http://qav.comlab.ox.ac.uk/papers/RR-08-01.pdf",
  year = "2008",
}


    
      @techreport{KKNP08c,
  author = "M. Kattenbelt and M. Kwiatkowska and G. Norman and D. Parker",
  institution = "Oxford University Computing Laboratory",
  month = "February",
  number = "RR-08-06",
  title = "A Game-based Abstraction-Refinement Framework for Markov Decision Processes",
  url = "http://qav.comlab.ox.ac.uk/papers/RR-08-06.pdf",
  year = "2008",
}