Bisimulation congruences in safe ambients

ABSTRACT

We study a variant of Levi and Sangiorgi's Safe Ambients (SA) enriched with passwords (SAP). In SAP by managing passwords, for example generating new ones and distributing them selectively, an ambient may now program who may migrate into its computation space, and when. Moreover in SAP an ambient may provide different services depending on the passwords exhibited by its incoming clients.We give an lts based operational semantics for SAP and a labelled bisimulation based equivalence which is proved to coincide with barbed congruence.Our notion of bisimulation is used to prove a set of algebraic laws which are subsequently exploited to prove more significant examples.

REFERENCES

• 1: Michele Bugliesi , Giuseppe Castagna , Silvia Crafa, Boxed Ambients, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.38-63, October 29-31, 2001
• 2: Luca Cardelli and Andrew Gordon. A commitment relation for the ambient calculus. Unpublished notes, 1996.
• 3: Luca Cardelli , Andrew D. Gordon, Types for mobile ambients, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.79-92, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292550]
• 4: Luca Cardelli , Andrew D. Gordon, Anytime, anywhere: modal logics for mobile ambients, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.365-377, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325742]
• 5: 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]
• 6: M. Hennessy and a. Rathke. Typed behavioural equivalences for processes in the presence of subtyping. Computer Science Report 2/01, University of Sussex, 2001.
• 7: Kohei Honda , Nobuko Yoshida, On reduction-based process semantics, Theoretical Computer Science, v.151 n.2, p.437-486, Nov. 27, 1995
• 8: 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]
• 9: M. Merro and M. Hennessy. Bisimulation congruences in safe ambients. Computer Science Report 5/01, University of Sussex, 2001.
• 10: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 11: 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]
• 12: Robin Milner , Davide Sangiorgi, Barbed Bisimulation, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.685-695, July 13-17, 1992
• 13: D. Sangiorgi. Eaprvssing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis CST 99-93, Department of Computer Science, University of Edinburgh, 1992.
• 14: Davide Sangiorgi, The lazy Lambda calculus in a concurrency scenario, Information and Computation, v.111 n.1, p.120-153, May 15 1994 [doi>10.1006/inco.1994.1042]
• 15: 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]
• 16: 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
• 17: 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
• 18: Maria Grazia Vigliotti. Transitions systems for the ambient calculus. Master thesis, Imperial College of Science, Technology and Medicine (University of London), September 1999.
• 19: Jan Vitek , Giuseppe Castagna, Seal: A Framework for Secure Mobile Computations, Workshop on Internet Programming Languages, p.47-77, May 13, 1998