Consistency Between the Predicate μ-Calculus and Modal Graphs
谓词μ演算和模态图的语义一致性

The modal graphs are effective graph forms for the predicate m-calculus. The consistency between the predicate m-calculus and the modal graphs is strictly established. Moreover, the relationship among the predicate m-calculus, nested predicate equations and the modal graphs is discussed in detail. An optimized transformation algorithm from predicate m-calculus formulae to nested predicate equations is presented.