| 摘要: |
| 带赋值符号迁移图是一般传值进程的语义模型,其强互模拟等价可以归结为谓词等式系的最大解.该文将这一结果推广到弱互模拟等价,为此,引入嵌套谓词等式系的概念,并提出算法,将带赋值符号迁移图的弱互模拟等价归结为形如E2μE1的嵌套谓词等式系的最大解. |
| 关键词: 传值进程,互模拟,谓词等式系. |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金和中国科学院“九五”基础研究重点项目基金资助. |
|
| Nesting Predicate Equation Systems and Weak Bisimulations |
|
LIN Hui-min
|
| 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. |
| Key words: Value-passing processes, bisimulation, predicate equation systems |
