Markov models are ubiquitous in decision-making and reasoning under uncertainty. A major branch of the formal verification for such models is probabilistic model checking. Numerous techniques and tools exist, and Christel Baier has been at the forefront of this area for decades. A particular branch of probabilistic model checking is the generation of counterexamples or explanations. In this paper, we reflect on some milestones in this area and highlight Christel’s contribution to shed light on the often opaque model checking results that are limited to numerical values or mere “yes” or “no” answers.