Behavioral theory for mobile ambients

ABSTRACT

We study a behavioral theory of Mobile Ambients, a process calculus for modelling mobile agents in wide-area networks, focussing on reduction barbed congruence. Our contribution is threefold. (1) We prove a context lemma which shows that only parallel and nesting contexts need be examined to recover this congruence. (2) We characterize this congruence using a labeled bisimilarity: this requires novel techniques to deal with asynchronous movements of agents and with the invisibility of migrations of secret locations. (3) We develop refined proof methods involving up-to proof techniques, which allow us to verify a set of algebraic laws and the correctness of more complex examples.

REFERENCES

• 1: Roberto M. Amadio , Ilaria Castellani , Davide Sangiorgi, On bisimulations of the asynchronous &pgr;-calculus, Theoretical Computer Science, v.195 n.2, p.291-324, March 30, 1998 [doi>10.1016/S0304-3975(97)00223-5 ]
• 2: S. Arun-Kumar , M. Hennessy, An efficiency preorder for processes, Acta Informatica, v.29 n.9, p.737-760, 1992
• 3: Boudol, G. 1992. Asynchrony and the π-calculus. Tech. Rep. RR-1702, INRIA-Sophia Antipolis.
• 4: Michele Bugliesi , Silvia Crafa , Massimo Merro , Vladimiro Sassone, Communication and mobility control in boxed ambients, Information and Computation, v.202 n.1, p.39-86, October 10, 2005 [doi>10.1016/j.ic.2005.06.002]
• 5: Luca Cardelli, Wide Area Computation, Proceedings of the 26th International Colloquium on Automata, Languages and Programming, p.10-24, July 11-15, 1999
• 6: Cardelli, L., and Gordon, A. 1996. A commitment relation for the ambient calculus. Unpublished notes.
• 7: Luca Cardelli , Andrew D. Gordon, Mobile ambients, Theoretical Computer Science, v.240 n.1, p.177-213, June 6 2000 [doi>10.1016/S0304-3975(99)00231-5 ]
• 8: G. Castagna , J. Vitek , F. Zappa Nardelli, The Seal Calculus, Information and Computation, v.201 n.1, p.1-54, 25 August 2005 [doi>10.1016/j.ic.2004.11.005]
• 9: De Nicola, R., and Hennessy, M. 1984. Testing equivalences for processes. Theoret. Comput. Sci. 34, 83--133.
• 10: Gian Luigi Ferrari , Ugo Montanari , Emilio Tuosto, A LTS Semantics of Ambients via Graph Synchronization with Mobility, Proceedings of the 7th Italian Conference on Theoretical Computer Science, p.1-16, October 04-06, 2001
• 11: Cédric Fournet , Georges Gonthier, A Hierarchy of Equivalences for Asynchronous Calculi, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.844-855, July 13-17, 1998
• 12: Jens Chr. Godskesen , Thomas Hildebrandt , Vladimiro Sassone, A Calculus of Mobile Resources, Proceedings of the 13th International Conference on Concurrency Theory, p.272-287, August 20-23, 2002
• 13: Andrew D. Gordon , Luca Cardelli, Equational properties of mobile ambients, Mathematical Structures in Computer Science, v.13 n.3, p.371-408, June 2003 [doi>10.1017/S0960129502003742]
• 14: Matthew Hennessy , Massimo Merro , Julian Rathke, Towards a behavioural theory of access and mobility control in distributed systems, Theoretical Computer Science, v.322 n.3, p.615-669, 6 September 2004 [doi>10.1016/j.tcs.2003.12.024]
• 15: Hennessy, M., Rathke, J., and Yoshida, N. 2003. Safedpi: A language for controlling mobile code. Computer Science Report 2003:02, University of Sussex.
• 16: James Riely , Matthew Hennessy, A typed language for distributed mobile processes (extended abstract), Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.378-390, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268978]
• 17: Hildebrandt, T., Godskesen, J. C., and Bundgaard, M. 2004. Bisimulation congruences for homer. Tech. Rep. TR-2004-52, ITU.
• 18: Daniel Hirschkoff , Étienne Lozes , Davide Sangiorgi, Separability, Expressiveness, and Decidability in the Ambient Logic, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.423-432, July 22-25, 2002
• 19: Kohei Honda , Mario Tokoro, An Object Calculus for Asynchronous Communication, Proceedings of the European Conference on Object-Oriented Programming, p.133-147, July 15-19, 1991
• 20: Kohei Honda , Nobuko Yoshida, On reduction-based process semantics, Theoretical Computer Science, v.151 n.2, p.437-486, Nov. 27, 1995
• 21: Douglas J. Howe, Proving congruence of bisimulation in functional programming languages, Information and Computation, v.124 n.2, p.103-112, Feb. 1, 1996 [doi>10.1006/inco.1996.0008 ]
• 22: Jeffrey, A., and Rathke, J. 2005. Contextual equivalence for higher-order π-calculus revisited. Log. Meth. Comput. Sci. 1, 1--4.
• 23: Jensen, O. H., and Milner, R. 2004. Bigraphs and mobile processes (revised). Tech. Rep. 580, LFCS, Dept. of Comp. Sci., Edinburgh Univ. Feb. (An extended abstract appeared in Conference Record of 30th Symposium on Principles of Programming Languages (POPL). ACM, New York, 2003.)
• 24: James J. Leifer , Robin Milner, Deriving Bisimulation Congruences for Reactive Systems, Proceedings of the 11th International Conference on Concurrency Theory, p.243-258, August 22-25, 2000
• 25: Francesca Levi , Davide Sangiorgi, Controlling interference in ambients, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.352-364, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325741]
• 26: Francesca Levi , Davide Sangiorgi, Mobile safe ambients, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.1, p.1-69, January 2003 [doi>10.1145/596980.596981]
• 27: Massimo Merro , Matthew Hennessy, Bisimulation congruences in safe ambients, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-80, January 16-18, 2002, Portland, Oregon
• 28: Massimo Merro , Matthew Hennessy, A bisimulation-based semantic theory of Safe Ambients, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.2, p.290-330, March 2006 [doi>10.1145/1119479.1119482]
• 29: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 30: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
• 31: Robin Milner , Davide Sangiorgi, Barbed Bisimulation, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.685-695, July 13-17, 1992
• 32: David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981
• 33: Sangiorgi, D. 1992. Expressing mobility in process algebras: First-order and higher-order paradigms. Ph.D. thesis, Dept. of Comp. Sci., Edinburgh University.
• 34: Davide Sangiorgi, Bisimulation for higher-order process calculi, Information and Computation, v.131 n.2, p.141-178, Dec. 15, 1996 [doi>10.1006/inco.1996.0096 ]
• 35: Davide Sangiorgi, Locality and interleaving semantics in calculi for mobile processes, Theoretical Computer Science, v.155 n.1, p.39-83, Feb. 26, 1996 [doi>10.1016/0304-3975(95)00020-8 ]
• 36: Davide Sangiorgi, On the bisimulation proof method, Mathematical Structures in Computer Science, v.8 n.5, p.447-479, October 1998 [doi>10.1017/S0960129598002527]
• 37: Davide Sangiorgi, Extensionality and intensionality of the ambient logics, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.4-13, January 2001, London, United Kingdom
• 38: Davide Sangiorgi , Robin Milner, The Problem of ``Weak Bisimulation up to'', Proceedings of the Third International Conference on Concurrency Theory, p.32-46, August 24-27, 1992
• 39: Davide Sangiorgi , David Walker, PI-Calculus: A Theory of Mobile Processes, Cambridge University Press, New York, NY, 2001
• 40: Davide Sangiorgi , David Walker, On Barbed Equivalences in pi-Calculus, Proceedings of the 12th International Conference on Concurrency Theory, p.292-304, August 20-25, 2001
• 41: Schmitt, A., and Stefani, J. 2004. The kell calculus: A family of higher-order distributed process calculi. In Lecture Notes in Computer Science, Springer-Verlag. Workshop of Global Computing.
• 42: Peter Sewell, From rewrite rules to bisimulation congruences, Theoretical Computer Science, v.274 n.1-2, p.183-230, March 6, 2002 [doi>10.1016/S0304-3975(00)00309-1 ]
• 43: Asis Unyapoth , Peter Sewell, Nomadic pict: correct communication infrastructure for mobile computation, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.116-127, January 2001, London, United Kingdom
• 44: Vigliotti, M. G. 1999. Transition systems for the ambient calculus. Master thesis, Imperial College of Science, Technology and Medicine (University of London).
• 45: Jan Vitek , Giuseppe Castagna, Seal: A Framework for Secure Mobile Computations, Workshop on Internet Programming Languages, p.47-77, May 13, 1998

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Process models

General Terms:
Languages, Theory

Keywords:
Behavioral theories, bisimulation, concurrency, process calculi, programming languages