摘要
并发计算是本质上不同于顺序计算的客观现象。许多并发计算模型相继被提出,试图能够像经典计算模型刻画顺序计算那样刻画并发计算。但是这些模型在许多方面缺乏统一的共识,比如基本运算符、操作语义、等价关系等等。这给并发计算的研究带来许多不便,特别是在程序等价、表达能力、图灵完备等领域,而这些又都是最基本的问题。
进程演算是一类并发计算模型的统称。它们的共同特点是以通信为基础,使用交错式并发语义等。前面所提到的问题在进程演算中尤为明显,具体表现为许多不同但又相似的演算模型,繁多的等价关系以及不一致的表达能力比较结果等。
交互理论正是为了给进程演算一个统一的框架而提出的。它把交互作为最基本的概念,在此基础上定义其他概念。本文的主要工作是在交互理论下重新研究了移动演算中的传名演算。作为交互理论的一个实例,我们重新研究了π演算,重点考察了其上模型独立的等价关系和证明系统。我们还在公平灰箱演算中引入测试等价,并考察了它的一些性质。
具体说来,本文从如下几个方面得到了一系列有关交互理论和模型独立观测理论的成果和创新:
?π演算上的观测理论研究
本文把传名演算的代表π演算在交互理论下进行再研究,主要是考察了其上的各种模型独立等价关系,包括引入新的测试等价。根据交互理论,进程行为的等价性判断应该是只能靠环境与其的交互,也就是环境对进程的观测来达到的。因而对于等价关系的研究我们称为观测理论,绝对等价在π演算中的形式也称为观测等价。我们的π演算将名区分为(常量)名和名变量。操作语义和等价关系的定义则遵照了交互理论的基本原则。这个新模型的表达能力不弱于原来的π演算,但是有着更加漂亮的理论结果和更好的实际应用价值。本文论证了在原来的π演算上的不同等价关系(barbed互模拟、标号互模拟、开互模拟、准开互模拟)都等同于由交互理论基本原则出发定义的观测互模拟。于是我们得到一个更一致的π演算,并且它的理论被大大简化。测试等价也以一种略有不同但更符合交互理论的形式被引入,它严格包含观测等价,符合直观,有着更好的性质。
?证明系统的研究
公理系统的研究始终是伴随着进程演算发展的。正因为等式公理给出了有关进程等价的代数规则,故进程演算又被称为进程代数。在本文中,研究对象称为证明系统而不是公理系统,是因为本文不是对某一等价关系进行公理化,得出一套等式公理,而是借公理系统的研究得到一套能够证明两个进程相等的系统推理方法。我们将在我们的π演算上,对观测等价和测试等价在有限进程上的证明系统进行考察。为了方便公理化,我们在π演算上引入了选择操作子,但这样会导致观测等价不同余,因为观测等价不在选择操作子下封闭。但是我们发现了P与Q观测等价当且仅当τ.P和τ.Q在公理系统中可证相等,这就给我们提供了一套观测等价的证明方法。我们对测试等价作了相似的研究,也得到了一套证明系统。本文还就有限控制进程的测试等价作了考察。通过进程方程组的刻画,同样给出了有限控制进程上的测试等价的证明系统。
?在公平灰箱演算上引入测试等价
公平灰箱演算(Fair Ambient,简称FA)是灰箱演算家族的成员之一。它通过在原有的移动灰箱演算(MobileAmbient)中加入补名,加强了对灰箱移入移出的控制。曾经有人研究过灰箱演算上的上下文等价,这是may测试等价的变体,是一种比较弱的等价关系。本文中定义的测试等价充分利用了补名的作用,也就是充分利用交互的性质,使得一部分特殊形式的测试者拥有所有测试者的区分能力。它在有限进程上是一个同余关系,在一类后继终止的进程上严格包含互模拟等价。本文还考察了两种不同的对成功状态的定义,一种是从结构的观点,另一种是从交互的观点。这两种定义得到的是相同的测试等价,这在某种程度上表明了交互理论的合理性。本文还就从π到FA的翻译在测试等价的意义下是否完全抽象作了研究,结果表明这个翻译仍然保持完全抽象。这为π演算是公平灰箱演算的一个子演算的观点增加了重要砝码。
本文对交互理论下的模型独立移动演算理论的所得到的研究成果,能够帮助人们深入理解交互理论。我们的π演算可以认为是在交互理论下重新认识进程演算的第一个实例,而对等价关系的研究表明进程演算中的等价关系能够统一到一个更加客观,独立于模型的关系。对于box等价的研究也显示出原本出发点很不相同的测试理论可以被很好地纳入交互理论。这些为进一步用交互理论研究进程演算、研究并发计算提供了非常有意义的尝试。
Concurrent computation is inherently different to sequential compu-tation. In the literature, researchers have proposed many concurrent mod-els in an effort to capture concurrent computation, trying to be as suc-cessful as classical computation models in capturing sequential computa-tion. However, these concurrent models lack some fundamental commonground, like basic operators, operational semantics and equivalence rela-tions. Consequently, it has many negative effects on the research of con-current computation, especially on program equality, expressiveness andTuring completeness, the most fundamental parts of concurrency theory.
Process calculi are mathematical models for describing and analysingproperties of concurrent computation with some characteristics in com-mon. These common points include the facts that they are based uponcommunication, that they are using interleaving semantics, etc. The neg-ative effects mentioned above affect process calculi even more apparently.We have a plethoral of similar but different calculi, many incompatibleequivalence relations, and chaotic results on expressiveness.
The theory of interaction of Fu has been proposed to give processcalculi a unified framework. It features interaction as the most basic prim-itive, upon which other concepts are build. The main contributions of thisthesis are investigations of model independent thoery of mobile calculiunder this framework. As a paradigm of the theory of interaction, we re-visit theπ-calculus of name-passing calculi, and compare the well-knownequivalence relations and proof systems on it. We also introduce testingequivalence into the Calculus of Fair Ambients.
The contributions of the thesis can be summarized as follows:
? Investigationsoftheobservationaltheoryareconductedonπ-calculus.We revisit theπ-calculus in the theory of interaction. Equalities onπ-calculus are investigated. These equalities include testing equiva-lence. Ourπ-calculus has disjoint sets of names and name variables.Its operational semantics and equivalence relation are redefined, ad-hering to the principles of the theory of interaction. The advantageof the new formulation is that it enjoys a simpler theory and is closerto computing practice. In this thesis, it is showed that many equiv-alence relations on the originalπ-calculus (barbed bisimilarity, la-belled bisimilarity, open bisimilarity, quasi-open bisimilarity) coin-cide with the observational bisimilarity, which is defined upon theprinciples of the theory of interaction. We have a more consistentπ-calculus with simplified theory. Testing equivalence is also intro-duced to theπ-calculus in a slightly different form.
? Proof systems of the observational equality and testing equivalenceare established.
Axiomatization is a crucial part of the research on process calculi.Because axioms provide us with algebraic rules about equivalencerelations, process calculi are also known as process algebra. In thisthesis we are concerning ourselves about proof systems rather thanaxiom systems. We are not axiomatizing particular equivalence re-lations, instead we construct systems which can prove whether twoprocesses are equivalent. In order to faciliate axiomatisation, we in-troduce unguarded choice. It breaks the congruence of observationalequality. We observe that P equals to Q if and only ifτ.P andτ.Qare provably equal in this system. This gives us a general method todecide whether two processes are observationally equal. A similartreatment is given to testing equivalence, for which we also obtain aproof system. We also investigate finite controlπ-processes. We give a proof system for box equivalence on finite controlπ-processes.
? Testing equivalence is defined and investigated for the Calculus ofFair Ambient.
The Calculus of Fair Ambient (FA for short) adds co-names to theCalculus of Mobile Ambient in order to strengthen the control ofambient movements. A variant of may testing equivalence, contex-tual equivalence, has been proposed for the Calculus Mobile Am-bient. But it is very weak. The testing equivalence defined in thisthesis exploits the functions of conames, making full use of inter-action. It is showed that the observers in some special form havethe full discriminating power that all observers have. It is a con-gruence on finite processes. On hereditarily terminating processesit strictly contains bisimilarity. It is also proved in this thesis thattwo definitions of successful states, one from a structural viewpointand another from an interactive viewpoint, result in the same testingequivalence relation. This justifies the theory of interaction to someextent. This thesis also investigates the encoding fromπ-calculus toFA, showing that it is also fully abstract with respect to the testingequivalence. This adds weights to the viewpoint thatπ-calculus is asubcalculus of FA.
The results in this thesis give us a deeper insight into both the theoryof interaction and name-passing calculi. ourπ-calculus can be consid-ered as a paradigm of redefining process calculi in the theory of interac-tion. The coincidence theory in this thesis tells that equivalence relationscan be unified to a single, objective and model independent relation. Boxequivalence also shows that testing equivalence, which is originally de-fined in a different style, can be integrated into the theory of interactionsmoothly. All theses results are of significance in reinforcing the view thatprocess calculi and concurrent computation should be investigated in asingle framework.
引文
[1] H. Lewis and C. Papadimitriou. Elements of the Theory of Computa-tion. Prentice Hall, 1997.
[2] M. Davis and E. Weyuker. Computability, Complexity, and Languages:Fundamentals of Theoretical Computer Science. Academic Press, 1983.
[3] H. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, 1984.
[4] L. Kari. DNA computing: Arrival of biological mathematics. TheMathematical Intelligencer, 19(2):9–22, 1997.
[5] M. Linial. On the potential of molecular computing. Science, 268:481–484, 1995.
[6] M. Hirvensalo. Quantum Computing. Springer, 2004.
[7] M. Nielsen and I. Chuang. Quantum Computation and Quantum In-formation. Cambridge University Press, 2000.
[8] J. McCarthy. A basis for a mathematical theory of computation.Computer Programming and Formal Systems, pages 33–70, 1963.
[9] G. Plotkin. A structural approach to operational semantics. Tech-nical Report FN-19, DAIMI, Computer Science Department, AarhusUniversity, 1981.
[10] G. Plotkin. The origins of structural operational semantics. Journalof Logic and Algebraic Programming, 2004.
[11] J. Stoy. Denotational Semantics: The Scott-Strachey Approach to Pro-gramming Language Theory. MIT Press, 1977.
[12] D. Scott and C. Strachey. Towards a mathematical semantics forcomputer languages. Technical Report PRG-6, Oxford University,1971.
[13] R. Floyd. Assigning meanings to programs. Mathematical Aspects ofComputer Science, 19:19–32, 1967.
[14] C. Hoare. An axiomatic basis for computer programming. Commu-nications of the ACM, 12(10):576–580, 1969.
[15] J. Baeten. The total order assumption. In Proceedings of the First NorthAmerican Process Algebra Workshop, pages 231–240. Springer, 1992.
[16] D. Park. Concurrency and automata on infinite sequences. LectureNotes in Computer Science, 104:167–183, 1981.
[17] F. Moller and P. Stevens. Edinburgh concurrency workbench usermanual. Available at http://www.dcs.ed.ac.uk/home/cwb/.
[18] B. Victor. A Verification Tool for the Polyadic-Calculus. PhD thesis,Licentiate thesis, Department of Computer Systems, Uppsala Uni-versity, 1994.
[19] J. Groote and M. Reniers. Algebraic process verification. In Handbookof Process Algebra, pages 1151–1208. Elsevier, 2001.
[20] J. Peterson. Petri Net Theory and the Modelling of Systems. Pretice Hall,1981.
[21] R. Milner. An approach to the semantics of parallel programs. InProceedings Convegno di informatica Teoretica, pages 285–301, 1973.
[22] R. Milner. Processes: A mathematical model of computing agents.Logic Colloquium, 73, 1975.
[23] R. Milner. Algebras for communicating systems. In Proceedings ofAFCET/SMF joint Colloquium in Applied Mathematics, 1978.
[24] R. Milner. Synthesis of communicating behavior. In Proceedings of7th Symposiom on Mathematical Foundations of Computer Science, vol-ume 64, pages 71–83, 1978.
[25] R. Milner. Flowgraphs and ?ow algebras. Journal of the ACM, 26(4):794–818, 1979.
[26] G. Milne and R. Milner. Concurrent processes and their syntax. Jour-nal of the ACM, 26(2):302–321, 1979.
[27] R. Milner. A calculus of communicating systems. Lcture Notes inComputer Science, 92, 1980.
[28] M. Hennessy and R. Milner. On Observing Nondeterminism and Con-currency. Springer, 1980.
[29] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
[30] J. Bergstra and J. Klop. Fixed point semantics in process algebras.Technical Report IW-206, Mathematical Center, Amsterdam, 1982.
[31] J. Baeten and W. Weijland. Process Algebra. Cambridge UniversityPress, 1991.
[32] J. Groote. Process Algebra and Structured Operational Semantics. PhDthesis, Universiteit van Amsterdam, 1991.
[33] C. Hoare. Communicating sequential processes. Communications ofthe ACM, 21(8):666–677, 1978.
[34] S. Brookes, C. Hoare, and A. Roscoe. A theory of communicatingsequential processes. Journal of the ACM, 31(3):560–599, 1984.
[35] C. Hoare. A model for communicating sequential processes. Tech-nical Report PRG-22, Computing Laboratory, University of Oxford,1981.
[36] E. Dijkstra. Guarded commands, nondeterminacy and formalderivation of programs. Communications of the ACM, 18(8):453–457,1975.
[37] S. Schneider. Concurrent and Real-Time Systems: The CSP Approach.John Wiley & Sons, 2000.
[38] P. Ryan, S. Schneider, G. Lowe, R. Roscoe, and M. Glodsmith. TheModelling and Analysis of Security Protocols. Addison Wesley, 2000.
[39] U. Engberg and M. Nielsen. A calculus of communicating systemswith label passing. Technical Report PB-208, DAIMI, Computer Sci-ence Department, University of Aarhus, 1986.
[40] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes,part i. Information and Computation, 100(1):1–40, 1992.
[41] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes,part ii. Information and Computation, 100(1):41–77, 1992.
[42] R. Milner. Communicating and Mobile Systems: TheπCalculus. Cam-bridge University Press, 1999.
[43] D. Sangiorgi. A theory of bisimulation for theπcalculus. In Proceed-ings of the 4th International Conference on Concurrency Theory (CON-CUR’93), pages 127–142. Springer, 1993.
[44] D. Sangiorgi and D. Walker. On barbed equivalences in pi-calculus.In Proceedings of the 12th International Conference on Concurrency The-ory (CONCUR’01), volume 2154 of Lecture Notes in Computer Science,pages 292–304. Springer, 2001.
[45] S. Mauw. PSF: A Process Specification Formalism. PhD thesis, Univer-siteit van Amsterdam, 1991.
[46] J. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, andM. Sighireanu. Cadp-a protocol validation and verification toolbox.In Proceedings of the 8th International Conference on Computer AidedVerification, pages 437–440, 1996.
[47] D. Sangiorgi and D. Walker. TheπCalculus: A Theory of Mobile Pro-cesses. Cambridge University Press, 2003.
[48] M. Fiore, E. Moggi, and D. Sangiorgi. A fully abstract model for theπcalculus. Information and Computation, 179(1):76–117, 2002.
[49] D. Sangiorgi. Termination of processes. Mathematical Structures inComputer Science, 16(1):1–39, 2006.
[50] G. Boudol. Asynchrony and theπcalculus (note). Technical Report1702, INRIA, 1992.
[51] K. Honda and M. Tokoro. On asynchronous communication seman-tics. In Proceedings of the Workshop on Object-Based Concurrent Com-puting, pages 21–51. Springer, 1991.
[52] K. Honda and M. Tokoro. An object calculus for asynchronous com-munication. In Proceedings of ECOOP’91, volume 91, pages 133–147,1991.
[53] D. Sangiorgi.πcalculus, internal mobility, and agent-passing cal-culi. Theoretical Computer Science, 167(1):235–274, 1996.
[54] R. Milner. The polyadic-calculus: A tutorial. Logic and Algebra ofSpecification, 94:91–180, 1993.
[55] M. Merro and D. Sangiorgi. On asynchrony in name-passing calculi.Mathematical Structures in Computer Science, 14(5):715–767, 2004.
[56] Yuxi Fu. Symmetricπ-calculus. Journal of Computer Science and Tech-nology, 13:202–208, 1998.
[57] Yuxi Fu. Theχ-calculus. In Advances in Computing Science, Proceed-ings of the 1997 International Conference on Advances in Parallel andDistributed Computing (APDC’97), pages 74–81. IEEE Computer So-ciety Press, 1997.
[58] Yuxi Fu. Bisimulation lattice of chi processes. In Proceedings of the4th Asian Computing Science Conference (ASIAN’98), volume 1538 ofLecture Notes in Computer Science, pages 245–262, Manila, The Philip-pines, December 1998. Springer.
[59] Yuxi Fu. Open bisimulations on chi processes. In Proceedings of the10th International Conference on Concurrency Theory (CONCUR’99),volume 1664 of Lecture Notes in Computer Science, pages 304–319,Eindhoven, The Netherlands, August 1999. Springer.
[60] Yuxi Fu and Zhengrong Yang. The ground congruence for chi cal-culus. In Proceedings of the 20th Conference on the Foundations of Soft-ware Technology and Theoretical Computer Science (FSTTCS’00), vol-ume 1974 of Lecture Notes in Computer Science, pages 385–396, NewDelhi, India, December 2000. Springer.
[61] Yuxi Fu. Bisimulation congruences of chi calculus. Information andComputation, 184:201–226, 2003.
[62] B. Pierce and D. Sangiorgi. Typing and subtyping for mobile pro-cesses. Mathematical Structures in Computer Science, 6(5):409–454,1996.
[63] N. Kobayashi, B. Pierce, and D. Turner. Linearity and the pi-calculus. ACM Transaction on Programming Languages and Systems,21(5):914–947, 1999.
[64] D. Sangiorgi. The name discipline of uniform receptiveness. Theo-retical Computer Science, 221(1-2):457–493, 1999.
[65] Xinxin Liu and D. Walker. A polymorphic type system for thepolyadic pi-calculus. In Proceedings of CONCUR’95, volume 962 ofLecture Notes in Computer Science, pages 103–116, 1995.
[66] L. Cardelli and A. Gordon. Mobile ambients. Theoretical ComputerScience, 240(1):177–213, 2000.
[67] F. Levi and D. Sangiorgi. Controlling interference in ambients. InProceedings of the 27th Symposium on Principles of Programming Lan-guages (POPL’00), pages 352–364. ACM Press, 2000.
[68] M. Merro and M. Hennessy. Bisimulation congruences in safe am-bients. In Proceedings of POPL’02, pages 71–80, 2002.
[69] D. Teller, P. Zimmer, and D. Hirschcoff. Using ambients to control re-sources. In Proceedings of CONCUR’02, volume 2421 of Lecture Notesin Computer Science, pages 288–303, 2002.
[70] X. Guan, Y. Yang, and J. You. Typing evolving ambients. InformationProcessing Letters, 80:265–270, 2001.
[71] Yuxi Fu. Fair ambients. Acta Informatica, 43(8):535–594, 2007.
[72] B. Thomsen. Plain chocs, a second generation calculus for higerorder processes. Acta Informatica, 30:1–59, 1993.
[73] B. Thomsen. Calculi for Higer Order Communicating Systems. PhDthesis, Imperial College, 1990.
[74] D. Sangiorgi. Expressing Mobility in Process Algebras: First-order andHigher-order Paradigms. PhD thesis, University of Edinburgh, 1992.
[75] J. Baeten. A brief history of process algebra. Theoretical ComputerScience, 335(2-3):131–146, 2005.
[76] L. Aceto. Some of my favorite results in classic process algebra.Technical Report NS-03-2, BRICS, 2003.
[77] J. Bergstra, A. Ponse, and S. Smolka. HandBook of Process Algebra.Elsevier, 2001.
[78] L. Aceto, Z. Esik, W. Fokkink, and A. Ingolfsdottir. Process algebra:Open problems and future directions. Technical Report NS-03-3,BRICS, 2003.
[79] R. Milner. Bigraphical reactive systems. Proceedings of the 12th Inter-national Conference on Concurrency Theory (CONCUR’01), pages 16–35, 2001.
[80] R. Milner. Calculi for interaction. Acta Informatica, 33(8):707–737,1996.
[81] R. Milner. Elements of interaction. Communication of the ACM, pages78–89, 1993.
[82] U. Nestmann. Welcome to the jungle: A subjective guide to mobileprocess calculi. In C. Baier and H. Hermanns, editors, Proceedingsof CONCUR’06, volume 4137 of Lecture Notes in Computer Science,pages 52–63, 2006.
[83] Yuxi Fu. Theory of interaction, 2008.
[84] Yuxi Fu and Hao Lu¨. On the expressiveness of interaction, 2007.Working Paper.
[85] C. Palamidessi. Comparing the expressive power of the syn-chronous and asynchronousπcalculi. Mathematical Structures inComputer Science, 13(05):685–719, 2003.
[86] U. Nestmann and B. Pierce. Decoding choice encodings. Informationand Computation, 163(1):1–59, 2000.
[87] M. Sipser. Introduction to the Theory of Computation. InternationalThomson Publishing, 1996.
[88] B. Thomsen. A theory of higher order communicating systems. In-formation and Compuatation, 116:38–57, 1995.
[89] B. Thomsen. A calculus of higher order communicating systems. InProceedings of POPL’89, pages 143–154, 1989.
[90] D. Sangiorgi. Fromπ-calculus to higher orderπ-calculus and back.In Proceedings of TAPSOFT’93, volume 668 of Lecture Notes in Com-puter Science, pages 151–166, 1993.
[91] R. Milner and D. Sangiorgi. Barbed bisimulation. In Proceedings ofthe 19th International Colloquium on Automata, Languages and Program-ming (ICALP’92), pages 685–695. Springer, 1992.
[92] R. de Nicola and M. Hennessy. Testing equivalences for processes.Theoretical Computer Science, 34:83–133, 1984.
[93] M. Boreale and R. de Nicola. Testing equivalence for mobile pro-cesses. Information and Computation, 120(2):279–303, 1995.
[94] D. Walker.π-calculus semantics for object oriented programminglanguages. In Proceedings of TACS’91, volume 526 of Lecture Notes inComputer Science, pages 532–547. Springer, 1991.
[95] D. Walker. Objects in theπ-calculus. Information and Computation,116:253–271, 1995.
[96] Huimin Lin. Complete inference systems for weak bisimulationequivalences in the pi-calculus. Information and Computation, 180(1):1–29, 2003.
[97] J. Parrow and D. Sangiorgi. Algebraic theories for name-passingcalculi. Information and Computation, 120:174–197, 1995.
[98] Xiaojuan Cai and Yuxi Fu. Programming in pi calculus, 2008.
[99] R. de Nicola and M. Hennessy. Testing equivalence for processes.In Proceedings of the 10th International Colloquium on Automata, Lan-guages and Programming (ICALP’83), pages 548–560. Springer, 1983.
[100] Yuxi Fu. Testing congruence for mobile process. Journal of ComputerScience and Technology, 17(1):73–82, 2002.
[101] R. Milner. Functions as processes. Technical Report 1154, INRIA,Sophia Antipolis, France, 1990.
[102] D. Sangiorgi and R. Milner. Techniques of“weak bisimulation upto”. In Proceedings of CONCUR’92, volume 630 of Lecture Notes inComputer Science, 1992.
[103] Yuxi Fu. On quasi open bisimulation. Theoretical Computer Science,338:96–126, 2005.
[104] Yuxi Fu. Variations on mobile processes. Theoretical Computer Sci-ence, 221:327–368, 1999.
[105] Huimin Lin. An interactive proof tool for process algebras. In Pro-ceedings of the 9th Annual Symposium on Theoretical Aspects of Com-puter Science, volume 577 of Lecture Notes in Computer Science, pages13–15. Springer, 1992.
[106] Yuxi Fu and Zhengrong Yang. Tau laws for pi calculus. TheoreticalComputer Science, 308:55–130, 2003.
[107] R. Milner. A complete axiomatisation for observational congruenceof finite-state behaviours. Information and Computation, 81:227–247,1989.
[108] Yuxin Deng, R. van Glabbeek, M. Hennessy, C. Morgan, and C.Zhang. Characterising testing preorders for finite probabilistic pro-cesses. In Proceedings of the 22nd Annual IEEE Symposium on Logic inComputer Science (LICS’07), pages 313–325. IEEE Computer Society,2007.
[109] A. Gordon and L. Cardelli. Equational properties of mobile am-bients. Mathematical Structures in Computer Science, 13(3):371–408,2003.
[110] M. Vigliotti and I. Phillips. Barbs and congruences for safe mobileambients. ENTCS, 66(3):37–51, 2002.
[111] M. Merro and M. Hennessy. A bisimulation-based semantic theoryof safe ambients. ACM Transactions on Programming Languages andSystems, 28(2):290–330, 2006.
[112] M. Merro and F. Zappa Nardelli. Bisimulation proof methods formobile ambients. In Proceedings of ICALP’03, 2003.
[113] J. Rathke and P. Sobocinski. Deriving structural labelled transitionsfor mobile ambients. In Proceedings of CONCUR’08, pages 462–476,2008.
[114] Yuxi Fu. Checking equivalence for higher order process. http://basics.sjtu.edu.cn/?yuxi/papers/LHO.pdf, 2006. Work-ing Paper.