摘要
带赋值符号迁移图是一般传值进程的语义模型,其强互模拟等价可以归结为谓词等式系的最大解.该文将这一结果推广到弱互模拟等价,为此,引入嵌套谓调等式系的概念,并提出算法,将带赋值符号迁移图的弱互模拟等价归结为形如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.
出处
《软件学报》
EI
CSCD
北大核心
1999年第11期1121-1126,共6页
Journal of Software
基金
国家自然科学基金
中国科学院"九五"基础研究重点项目