在高阶CCS中表达一阶π演算

摘要: Thomsen和Sangiorgi对高阶进程演算（分别是高阶CCS和高阶π演算）与一阶π演算之间的相互编码进行了研究，但他们的工作尚不完整，缺少对用高阶CCS对一阶π演算编码的全抽象性质的深入研究。在本文中，我们进一步研究这一问题并得到关于全抽象的有意义的结论，从而补充了上述关于高阶进程演算对一阶进程演算的编码的研究，同时为类似的关于进程演算之间的表达能力的关系的研究提供了参考。我们基于Thomsen的编码方法，将一阶π演算翻译到Plain CHOCS（一种高阶CCS）中。我们证明这种编码方法在早互模拟性（一阶π演算中）和线缆互模拟性（Plain CHOCS中）下是全抽象的，其中线缆互模拟性是我们定义的基于仅发送和接收线缆（wire）的线缆进程的一种互模拟，它们是编码策略的核心。所谓全抽象，其意义是两个一阶π演算进程P,Q是早互模拟的，当且仅当它们的编码P, Q是线缆互模拟的。进一步，由于wired互模拟性蕴含广为人知的上下文互模拟性，我们确保了在早互模拟性和上下文互模拟性下编码的可靠性。所谓可靠性，是指如果两个一阶π演算进程P,Q是早互模拟的，那么它们的编码P, Q是上下文互模拟的。我们使用领域中已有的索引技术来处理技术细节中的难点以获得主要结论，即将索引技术应用到原始编码方法中，以此来处理编码中产生的额外内部动作，随后将带索引的编码方法中所获得的结果移植得到原始编码中的相应结论。我们还讨论了如何通过在两个演算中选择合理的互模拟来获得全抽象性质等问题；所得到的结论告诉我们，选取演算中合理的、符合直观的互模拟，是获得合理的编码性质的重要因素。基于我们已有的工作，可以进一步研究几个问题。首先，这里研究的从一阶π演算到Plain CHOCS的编码可以用于提供另一种用高阶进程演算编码λ演算的途径，我们可以进一步细化其中的细节。其次，我们很想知道若不使用重命名操作子，是否仍然有相应的编码，若存在，我们需要考察其是否是全抽象的，否则，我们应该给出负面结论的证明，后者通常并不容易。再次，我们可以尝试使用完整的演算，即在一阶π演算中保留选择操作子，这可能需要另一种不同的方法和技术路线。不同演算之间的编码是比较它们的表达能力的有效方法，可以揭示它们之间的本质区别。在研究中精确定位一个演算在进程演算体系中所处的地位有下面几点意义。一点是，如果我们可以证明它可以被编码（表达）为其它的已经较完备的演算且反之亦然，那么这个新的演算只是提供了另一个可选的建模工具，其计算能力中没有新的内容。另一点是，如果新的演算被证明严格地包含了已知计算能力的某种演算，则这种演算在建模和计算方面都更有价值。我们的研究从一个方面补充完善了高阶进程演算与一阶进程演算之间关系的研究，为进一步研究其它相关演算提供了借鉴，并且从另一方面为相关的应用创造了理论前提，即某种意义上，高阶进程演算可以用在多种应用领域的系统建模、分析等过程中，并保持与一阶进程演算具有相当的表达能力。这些领域包括如生物计算、安全协议分析验证、各种网络应用（如web service及网格计算）的辅助分析检测等等。

Abstract: In the study of process calculi, encoding between different calculiis an effective way to compare the expressive power of calculi and canshed light on the essence of where the difference lies. Thomsen andSangiorgi have worked on the higher-order calculi (higher-order Calculusof Communicating Systems (CCS) and higher-order \pi-calculus, respectively) and the encodingfrom and to first-order \pi-calculus. However a fully abstractencoding of first-order \pi-calculus with higher-order CCS isnot available up-today. This is what we intend to settle in thispaper. We follow the encoding strategy, first proposed by Thomsen, oftranslating first-order \pi-calculus into Plain CHOCS. We show that theencoding strategy is fully abstract with respect to earlybisimilarity (first-order \pi-calculus) and wired bisimilarity(Plain CHOCS) (which is a bisimulation defined on wired processes only sendingand receiving wires), that is the core of the encoding strategy.Moreover from the fact that the wired bisimilarity is contained by thewell-established context bisimilarity, we secure the soundness ofthe encoding, with respect to early bisimilarity and contextbisimilarity. We use index technique to get around all the technicaldetails to reach these main results of this paper. Finally, we makesome discussion on our work and suggest some future work.

在高阶CCS中表达一阶π演算

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