谓词μ演算和模态图的语义一致性  

Consistency Between the Predicate μ-Calculus and Modal Graphs

作　　者：刘剑[1] 林惠民[1] 

机构地区：[1]中国科学院软件研究所计算机科学重点实验室,北京100080

出　　处：《软件学报》2003年第10期1672-1680,共9页Journal of Software

基　　金：国家自然科学基金~~

摘　　要：模态图是谓词m演算的一种有效的图形表示形式.证明了谓词m演算和模态图的语义一致性,详细讨论了谓词m演算公式、嵌套谓词等式系和模态图之间的关系,并给出了一种优化的从线性公式到嵌套谓词等式系的转换算法.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.

关 键 词：不动点 谓词μ演算 嵌套谓词等式系 模态图 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]