摘要：A mu-calculus over dependence graph representation of traces is considered. It is shown that the mu-calculus cannot express all monadic second order (MSO) properties of dependence graphs. Several extensions of the mu-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.
