ABSTRACT. One of the claimed advantages of model checking is its capability to provide a counter-example explaining why a property is violated by a given system. Nevertheless, branching logics such as Computation Tree Logic and its extensions have complex branching counter-examples, and standard model checkers such as NuSMV do not produce complete counter-examples and are limited to single executions. Many branching logics can be translated into the mu-calculus. To solve this problem of producing complete and complex counter-examples for branching logics, we propose a mu-calculus-based framework with rich explanations. It integrates a mu-calculus model checker that produces complete explanations, and several functionalities to translate them back to the original logic. In addition to the framework itself, we describe its implementation in Python and illustrate its applicability with Alternating Temporal Logic.