Tableaux and witnesses for the my--calculus

Symbolic temporal logic model checking is an automatic verification method. One of its main features is that a counterexample can be constructed when a temporal formula does not hold for the model. Most model checkers so far have restricted the type of formulae that can be checked and for which counterexamples can be constructed to fair CTL formulae. This paper shows how counterexamples and witnesses for the whole µ-Calculus can be constructed. The witness construction presented in this paper is polynomial in the model and the formula