2

Abstract. We report on new strategies for model checking quantita-tive reachability properties of Markov decision processes by successive renements. In our approach, properties are analyzed on abstractions rather than directly on the given model. Such abstractions are expected to be signicantly smaller than the original model, and may safely refute or accept the required property. Otherwise, the abstraction is rened and the process repeated. As the numerical analysis involved in settling the validity of the property is more costly than the renement process, the method prots from applying such numerical analysis on smaller state spaces. The method is signicantly enhanced by a number of novel strategies: a strategy for reducing the size of the numerical problems to be analyzed by identication of so-called essential states, and heuristic strategies for guiding the renement process.