The early success story of the model checking approach relies fundamentally on two features. First, the algorithms provide a push-button technology: As soon as the model and specification have been generated, one obtains a result in a fully automated way. Second, if the algorithm terminates with a negative result, then it can infer counterexamples to the specification. Counterexamples are the first instances for what we use the term explication, which refers to a mathematical concept that in some way sheds light on why the model checker has returned the result. While counterexamplesare single instances of execution traces violating the specification, they provide little insights in what causes the specification violation. To enhance the system transparency, more crisp explications for the satisfaction or violation of properties are demanded. The talk presents an overviewof techniques that go in this direction by using formal notions of causality and responsibility to explicate verification results for transition systems and Markovian models.