嵌套谓词等式系与弱互模拟  

Nesting Predicate Equation Systems and Weak Bisimulations

作　　者：林惠民[1] 

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

出　　处：《软件学报》1999年第11期1121-1126,共6页Journal of Software

基　　金：国家自然科学基金;中国科学院"九五"基础研究重点项目

摘　　要：带赋值符号迁移图是一般传值进程的语义模型，其强互模拟等价可以归结为谓词等式系的最大解．该文将这一结果推广到弱互模拟等价，为此，引入嵌套谓调等式系的概念，并提出算法，将带赋值符号迁移图的弱互模拟等价归结为形如E2μE1的嵌套谓词等式系的最大解．Symbolic transition graphs with assignment is a general semantical model for value-passing pro-cesses. Strong bisimulation equivalences between such graphs can be reduced t0 the greatest solutions to simplepredicate equation systems. The aim of this paper is to generalise this result to weak bisimulation equivalences.For this purpose, the notion of nesting predicate equation systems is introduced, and algorithms are presentedto reduce weak bisimulation equivalences to the greatest solutions to nesting predicate equation systems of theform E2μE1.

关 键 词：传值进程 互模拟 谓词等式系 符号迁移图 算法 

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