On model checking for the μ-calculus and its fragments

In this paper, we consider the model checking problem for the μ-calculus and show that it is succinctly equivalent to the non-emptiness problem of finite-state automata on infinite binary trees with the parity acceptance condition. We also present efficient model checking algorithms for two rich subclasses of the μ-calculus formulas and relate their expressive power to well-known extensions of branching time temporal logics.