一个移动进程演算的互模拟同余定义框架

A Bisimulation Congruence Definition Framework for Mobile Process Calculi

并发计算模型是理论计算机科学研究的重要领域之一。以π演算为代表的移动进程演算是目前并发理论的研究热点。互模拟等价定义是移动进程演算研究中的核心概念和问题,而传名机制使得移动进程演算中的互模拟同余关系更加复杂和有趣。本文在分析了常见的互模拟同余定义的基础上,通过抽取定义的核心要素,提出了一个三维的互模拟同余定义模型,从而将一般文献中常见的互模拟定义纳入到一个统一的框架中来,加深了我们对移动进程演算中互模拟概念的理解;同时本文利用这个模型,系统分析了各种互模拟之间的关系。模型的优点在于它的普适性和开放性。

Concurrent computation model is one of the most important fields in theoretical computer science. Mobile process calculus, notably π calculus, is one of the hottest fields in concurrent theory. Bisimulation equivalence is the key concept and problem in the research of this kind of calculus. However, the name-passing mechanism makes the definition of bisimulation congruence more intricacy and interesting. Based on our understanding of common bisimulation congruence definitions, a very generic framework is proposed for analysis and systematic study of such definitions. Most of common bisimulation congruence can be embedded in this uniform model, which provides some insight into bisimulation congruence in mobile process calculus; based on this model, the relations between these congruence relations are systematically studied and can be specified in a uniform and clear way. The main merits of this framework lie in its generality and openness.