移动进程演算中的开互模拟  

An Open Problem of Mobile Processes

作　　者：傅育熙[1] 

机构地区：[1]上海交通大学计算机科学与工程系,上海200030

出　　处：《计算机学报》2001年第7期673-679,共7页Chinese Journal of Computers

基　　金：国家自然科学基金 (69873 0 3 2 );教育部优秀青年教师资助项目;高等学校骨干教师资助计划;上海高校软件理论研究中心

摘　　要：该文就移动进程演算中的弱开同余关系进行研究 .文中考虑了一种简单的非确定性移动进程演算模型 ,证明了 Milner的三条 tau规则在有等名测试算子时不足以将强开同余关系的完全公理化系统提升到弱开同余关系的完全公理化系统 .文中提出了第四条 tau规则 ,处理了在前缀操作下的等名测试算子 ,并证明了强开同余关系的完全公理化系统加上四条 tau规则可得到弱开同余关系的完全公理化系统 .该文的结论否定了关于 Milner的三条Over the last decade calculi of mobile processes have been a focus in process algebra. The interest in such calculi arises from the following facts: Firstly mobile processes model some modern concepts of computation such as object oriented computation, which is impossible using traditional process calculi such as CCS. Secondly the algebraic theory of mobile processes is a lot more subtle than that for CCS. For one thing there are many weak bisimulation congruence relations for mobile processes, some of them have not been well understood.This paper takes a look at open weak congruence in calculi of mobile processes.By focusing on a simple calculus of nondeterministic mobile processes, it is proved that Milner's three tau laws fail to lift a complete system for strong open congruence to a complete system for weak open congruence in the presence of match operator. A fourth tau law is proposed that deals with match operator under prefix operation. It is shown that a complete system for the strong open congruence extended with all the four tau laws is complete for the weak open congruence. The result of this paper refutes the general belief that Milner's tau laws are enough to lift a complete system for a strong congruence to a complete system for the corresponding weak congruence in π calculus.

关 键 词：进程代数 互模拟 公理化 移动进程演算 计算机 

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