@inproceedings{WZ10,
  author = {Bj\"orn Wachter and Lijun Zhang},
  title = {Best Probabilistic Transformers},
  booktitle = {VMCAI},
  year = {2010},
  pages = {362-379},
  subproject  =   {S2,S3},
  access = {restricted},
  bibtex={wachter.vmcai10.bib},
  pdf={wachter.vmcai10.pdf},
  abstract = {
  This paper investigates relative precision and optimality of
  analyses for concurrent probabilistic systems. Aiming at the problem at
  the heart of probabilistic model checking – computing the probability of
  reaching a particular set of states – we leverage the theory of abstract
interpretation.
  With a focus on predicate abstraction, we develop the first
  abstract-interpretation framework for Markov decision processes which
  admits to compute both lower and upper bounds on reachability
probabilities.
  Further, we describe how to compute and approximate such
  abstractions using abstraction refinement and give experimental results.
  }
}