Reference

[WachterZ10] Wachter, B. and Zhang, L. Best Probabilistic Transformers. In VMCAI, pages 362-379, Springer, 2010.
Downloads: pdf, bibAbstract. 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 in- terpretation. 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 prob- abilities. Further, we describe how to compute and approximate such abstractions using abstraction refinement and give experimental results.