Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems  

作　　者：徐贤 

机构地区：[1]Department of Computer Science and Engineering,Shanghai Jiao Tong University [2]Department of Computer Science and Engineering,East China University of Science and Technology

出　　处：《Journal of Computer Science & Technology》2009年第1期122-137,共16页计算机科学技术学报（英文版）

基　　金：supported by the National Basic Research 973 Program of China under Grant No.2003CB317005;the National Natural Science Foundation of China under Grant Nos.60473006 and 60573002;the National Research Foundation for the Doctoral Program of Higher Education of China Research Fund under Grant No.20010248033.

摘　　要：In the study of process calculi, encoding between different calculi is an effective way to compare the expressive power of calculi and can shed light on the essence of where the difference lies. Thomsen and Sangiorgi have worked on the higher-order calculi （higher-order Calculus of Communicating Systems （CCS） and higher-order π-calculus, respectively） and the encoding from and to first-order π-calculus. However a fully abstract encoding of first-order π-calculus with higher-order CCS is not available up-today. This is what we intend to settle in this paper. We follow the encoding strategy, first proposed by Thomsen, of translating first-order π-calculus into Plain CHOCS. We show that the encoding strategy is fully abstract with respect to early bisimilarity （first-order π-calculus） and wired bisimilarity （Plain CHOCS） （which is a bisimulation defined on wired processes only sending and receiving wires）, that is the core of the encoding strategy. Moreover from the fact that the wired bisimilarity is contained by the well-established context bisimilarity, we secure the soundness of the encoding, with respect to early bisimilarity and context bisimilarity. We use index technique to get around all the technical details to reach these main results of this paper. Finally, we make some discussion on our work and suggest some future work.In the study of process calculi, encoding between different calculi is an effective way to compare the expressive power of calculi and can shed light on the essence of where the difference lies. Thomsen and Sangiorgi have worked on the higher-order calculi （higher-order Calculus of Communicating Systems （CCS） and higher-order π-calculus, respectively） and the encoding from and to first-order π-calculus. However a fully abstract encoding of first-order π-calculus with higher-order CCS is not available up-today. This is what we intend to settle in this paper. We follow the encoding strategy, first proposed by Thomsen, of translating first-order π-calculus into Plain CHOCS. We show that the encoding strategy is fully abstract with respect to early bisimilarity （first-order π-calculus） and wired bisimilarity （Plain CHOCS） （which is a bisimulation defined on wired processes only sending and receiving wires）, that is the core of the encoding strategy. Moreover from the fact that the wired bisimilarity is contained by the well-established context bisimilarity, we secure the soundness of the encoding, with respect to early bisimilarity and context bisimilarity. We use index technique to get around all the technical details to reach these main results of this paper. Finally, we make some discussion on our work and suggest some future work.

关 键 词：process calculus higher order BISIMULATION encoding full abstraction 

分 类 号：TN914[电子电信—通信与信息系统]