Journal of Software:1999.10(11):1121-1126

Nesting Predicate Equation Systems and Weak Bisimulations
LIN Hui-min
Chart / table
Similar Articles
Article :Browse 2430   Download 2276
Received:August 20, 1998    Revised:December 25, 1998
> 中文摘要: 带赋值符号迁移图是一般传值进程的语义模型,其强互模拟等价可以归结为谓词等式系的最大解.该文将这一结果推广到弱互模拟等价,为此,引入嵌套谓词等式系的概念,并提出算法,将带赋值符号迁移图的弱互模拟等价归结为形如E2μE1的嵌套谓词等式系的最大解.
Abstract:Symbolic transition graphs with assignment is a general semantical model for value-passing processes. Strong bisimulation equivalences between such graphs can be reduced to the greatest solutions to simple predicate 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 presented to reduce weak bisimulation equivalences to the greatest solutions to nesting predicate equation systems of the form E2μE1.
文章编号:     中图分类号:    文献标志码:
基金项目:本文研究得到国家自然科学基金和中国科学院“九五”基础研究重点项目基金资助. 本文研究得到国家自然科学基金和中国科学院“九五”基础研究重点项目基金资助.
Foundation items:
Reference text:


LIN Hui-min.Nesting Predicate Equation Systems and Weak Bisimulations.Journal of Software,1999,10(11):1121-1126