Process Passing Calculus, Revisited

doi:10.1007/s12204-013-1365-6

Abstract

Abstract: In the context of process calculi, higher order π calculus (Λ calculus) is prominent and popular due to its ability to transfer processes. Motivated by the attempt to study the process theory in an integrated way, we give a system study of Λ calculus with respect to the model independent framework. We show the coincidence of the context bisimulation to the absolute equality. We also build a subbisimilarity relation from Λ calculus to the π calculus.

Key words: higher order π-calculus| encoding| expressiveness| bisimulation

摘要： In the context of process calculi, higher order π calculus (Λ calculus) is prominent and popular due to its ability to transfer processes. Motivated by the attempt to study the process theory in an integrated way, we give a system study of Λ calculus with respect to the model independent framework. We show the coincidence of the context bisimulation to the absolute equality. We also build a subbisimilarity relation from Λ calculus to the π calculus.

关键词: higher order π-calculus| encoding| expressiveness| bisimulation

CLC Number:

TP 301.2

YIN Qiang* (尹强), LONG Huan (龙环). Process Passing Calculus, Revisited[J]. Journal of shanghai Jiaotong University (Science), 2013, 18(1): 29-36.

References

[1] Sangiorgi D. Expressing mobility in process algebras: First-order and higher-order paradigms [D]. Edinburgh: Department of Computer Science, University of Edinburgh, 1992.
[2] Milner R. Communication and concurrency [M]. Upper Saddle River, NJ: Prentice-Hall, Inc., 1989.
[3] Milner R, Parrow J, Walker D. A calculus of mobile process, part I/II [J]. Journal of Information and Computation, 1992, 100: 1-77.
[4] Sangiorgi D. Bisimulation for higher-order process calculi [J]. Information and Computation, 1996, 131(2): 141-178.
[5] Sangiorgi D, Kobayashi N, Sumii E. Environmental bisimulations for higher-order languages [J]. ACM Transactions on Programming Languages and Systems, 2011, 33(1): 5-15.
[6] Fu Y. Theory of interaction [EB/OL]. (2011-10-24).http://basics.sjtu.edu.cn/～yuxi.
[7] van Glabbeek R J. The linear time—branching time spectrum II [C]//Proceedings of 4th International Conference on Concurrency Theory. Heidelberg: Springer-Verlag, 1993: 66-81.
[8] Palamidessi C. Comparing the expressive power of the synchronous and asynchronous pi-calculi [J]. Mathematical Structures in Computer Science, 2003, 13(5): 685-719.
[9] Gorla D. Towards a unified approach to encodability and separation results for process calculi [J]. Journal of Information and Computation, 2010, 208(9): 1031-1053.
[10] Nain S, Vardi M Y. Trace semantics is fully abstract [C]// Proceedings of the 2009 24th Annual IEEE Symposium on Logic in Computer Science. Washington: IEEE, 2009: 59-68.
[11] Thomsen B. A calculus of higher order communicating systems [C]//Proceedings of the 16th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. New York: ACM, 1989: 143-154.
[12] Thomsen B. Calculi for higher order communicating systems [D]. London: Imperial College of Science, Technology and Medicine, University of London, 1990.
[13] Amadio R M. On the reduction of chocs bisimulation to π-calculus bisimulation [C]//Proceedings of 4th International Conference on Concurrency Theory. Heidelberg: Springer-Verlag, 1993: 112-126.
[14] Sangiorgi D. From pi-calculus to higher-order picalculus and back [C]// Proceedings of International Joint Conference on Theory and Practice of Software Development. Heidelberg: Springer-Verlag, 1993: 151-166.
[15] Fu Y, Lu H. On the expressiveness of interaction [J]. Theoretical Computer Science, 2010, 411(11-13): 1387-1451.
[16] Fu Y, Zhu H. The name-passing calculus [EB/OL]. (2011-10-24). http://basics.sjtu.edu.cn/～yuxi.