Best Probabilistic Transformers
In Verification, Model Checking, and Abstract
Interpretation, 11th International Conference
, pages 362-379, Springer
, Lecture Notes in Computer Science 5944, 2010.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-11319-2_26
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.