Model checking has been extensively used to automatically check properties in large-scale systems. However, the classical techniques only allow for checking of qualitative properties, thus being inadequate for inherently probabilistic systems. Probabilistic model checking (PMC) extends the classical suite of techniques of classical model checking by allowing quantitative reasoning over probabilistic-nondeterministic systems which combine both probabilistic behaviour and nondeterministic choice. Abstraction, the main tool to deal with the “state explosion” problem in the classical setting, is not well developed in the probabilistic setting, limiting the applicability of PMC to little more than checking of reachability properties. Part of the reason for this limited success is that counterexamples in the probabilistic cases are much more complicated objects than their classical counterparts, making counterexample analysis much harder. In this seminar, we will present an abstraction-refinement loop for probabilistic systems based on an extension of the concept of may and must abstractions in the classical setting. May and must abstractions are respectively over and underestimations of the behaviours of a system. For a large class of properties, one of the abstractions preserves satisfaction and the other preserves non-satisfaction, eliminating the need for (expensive) counterexample analysis. Joint work with Anvesh Komuravelli and Edmund Clarke.