Best Probabilistic Transformers

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 intion. With a focus on predicate abstraction, we develop the first 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 ions using abstraction refinement and give experimental results.

• Type: Conference
• Year: 2010
• Where: VMCAI
• Authors: Björn Wachter, Lijun Zhang
• Keywords: Concurrent Probabilistic Systems, Markov Decision Processes, Probabilistic Model Checking, Software Engineering, VMCAI 2010