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

An Open Problem of Mobile Processes

该文就移动进程演算中的弱开同余关系进行研究 .文中考虑了一种简单的非确定性移动进程演算模型 ,证明了 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.