The µ-calculus over dependence graph representation of traces is considered. It is shown that the plain µ-calculus cannot express all monadic second-order (MSO) properties of dependence graphs. Several extensions of the µ-calculus are presented and it is proved that these extensions are equivalent in expressive power to MSO logic. The satisfiability problem for these extensions is PSPACE-complete.
Journal of Automata, Languages and Combinatorics, 2002, Vol 7, Issue 2, p. 259-290