Journal of Software
1000-9825
2003
14
10
1672
1680
article
谓词μ演算和模态图的语义一致性
Consistency Between the Predicate μ-Calculus and Modal Graphs
模态图是谓词μ演算的一种有效的图形表示形式.证明了谓词μ演算和模态图的语义一致性,详细讨论了谓词μ演算公式、嵌套谓词等式系和模态图之间的关系,并给出了一种优化的从线性公式到嵌套谓词等式系的转换算法.
The modal graphs are effective graph forms for the predicate μ-calculus. The consistency between the predicate μ-calculus and the modal graphs is strictly established. Moreover, the relationship among the predicate μ-calculus, nested predicate equations and the modal graphs is discussed in detail. An optimized transformation algorithm from predicate μ-calculus formulae to nested predicate equations is presented.
不动点;谓词μ演算;嵌套谓词等式系;模态图
fixed-point; predicate μ-calculus; nested predicate equation; modal graph
刘剑,林惠民
LIU Jian and LIN Hui-Min
jos/article/abstract/20031002