×

Name-passing in an ambient-like calculus and its proof using spatial logic. (English) Zbl 1092.68067

Summary: This paper studies a restricted version of the ambient calculus, a process model for mobile and distributed computation. We only allow single-threaded ambients migrating in a network of immobile ambients, exchanging payloads, and delivering them. With this restriction, we arrive at a calculus free from grave interferences. In previous works, this is only possible by sophisticated type systems.
We focus on the expressiveness of the restricted calculus. We show that we can still repeat Zimmer’s encoding of name-passing in our calculus. Moreover, we prove a stronger operational correspondence result than Zimmer’s. The proof takes advantage on a specification about the spatial structure and process distributions of the encoding that are invariant to reductions, using a novel spatial logic.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

SLMC
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Amtoft, T.; Makholm, H.; Wells, J. B., PolyA: true type polymorphism for mobile ambients, (Levy, J.-J.; Mayr, E. W.; Mitchell, J. C., Proc. TCS 2004 (2004), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 591-604 · Zbl 1088.68653
[2] Berry, G.; Boudol, G., The chemical abstract machine, Theoret. Comput. Sci., 96, 217-248 (1992) · Zbl 0747.68013
[3] Bugliesi, M.; Castagna, G.; Crafa, S., Access control for mobile agents: the calculus of boxed ambients, ACM Trans. Programming Languages Systems, 26, 1, 57-124 (2004)
[4] Caires, L.; Cardelli, L., A spatial logic for concurrency (part i), Inform. and Comput., 186, 2, 194-235 (2003) · Zbl 1068.03022
[5] Cardelli, L., Abstraction for mobile computation, (Vitek, J.; Jensen, C., Secure Internet Programming, Lecture Notes in Computer Science, Vol. 1603 (1999), Springer: Springer Berlin), 51-94
[6] Cardelli, L.; Gardner, P.; Ghelli, G., Manipulating trees with hidden labels, (in: Proc. FoSSaCS 2003, Lecture Notes in Computer Science, Vol. 2620 (2003), Springer: Springer Berlin), 216-232 · Zbl 1029.68092
[7] Cardelli, L.; Gordon, A. D., Mobile ambients, Theoret. Comput. Sci., 240, 1, 177-213, (2000), An extended abstract appeared in Proc. FoSSaCS ’98, pp. 140-155 · Zbl 0954.68108
[8] Cardelli, L.; Gordon, A. D., Anytime anywhere: modal logics for mobile ambients, (Proc. POPL ’00 (January 2000), ACM: ACM New York), 365-377 · Zbl 1323.68405
[9] Cardelli, L.; Gordon, A. D., Logical properties of name restriction, (in: Proc. TLCA 2001, Lecture Notes in Computer Science, Vol. 2044 (2001), Springer: Springer Berlin) · Zbl 0981.68036
[10] M. Coppo, M. Dezani-Ciacaglini, E. Giovannetti, I. Salvo, M3: mobility types for mobile processes in mobile ambients, in: Proc. CATS 2003, ENTCS, Vol. 78, 2003.; M. Coppo, M. Dezani-Ciacaglini, E. Giovannetti, I. Salvo, M3: mobility types for mobile processes in mobile ambients, in: Proc. CATS 2003, ENTCS, Vol. 78, 2003. · Zbl 1270.68211
[11] Dal-Zilio, S.; Lugiez, D.; Meyssonnier, C., A logic you can count on, (Proc. POPL 2004 (2004), ACM Press: ACM Press New York), 135-146 · Zbl 1325.03032
[12] Gordon, A. D.; Cardelli, L., Equational properties of mobile ambients, (Thomas, W., Proc. FoSSaCS ’99, Lecture Notes in Computer Science, Vol. 1578 (1999), Springer: Springer Berlin), 212-226 · Zbl 1085.68099
[13] Guan, X., Towards a tree of channels, (Sassone, V., Electronic Notes in Theoretical Computer Science, Vol. 85 (2003), Elsevier: Elsevier Amsterdam)
[14] Hennessy, M.; Riely, J., Resource access control in systems of mobile agents, J. Inform. and Comput., 173, 1, 82-120, (2002), An extended abstract appeared in Proc. HLCL’98, pp. 3-17 · Zbl 1009.68081
[15] Levi, F.; Sangiorgi, D., Mobile safe ambients, Trans. Programming Languages Systems, 25, 1, 1-69 (2003)
[16] S. Maffeis, I. Phillips, On the computational strength of pure ambient calculi, in: Proc. Express 2003, ENTCS, Vol. 91, 2003.; S. Maffeis, I. Phillips, On the computational strength of pure ambient calculi, in: Proc. Express 2003, ENTCS, Vol. 91, 2003. · Zbl 1271.68190
[17] M. Merro, M. Hennessy, Bisimulation congruences in safe ambients, in: Proc. POPL 2002, 2002, pp. 71-80.; M. Merro, M. Hennessy, Bisimulation congruences in safe ambients, in: Proc. POPL 2002, 2002, pp. 71-80. · Zbl 1323.68412
[18] Merro, M.; Nardelli, F. Z., Bisimulation proof methods for mobile ambients, (Proc. ICALP 2003, Lecture Notes in Computer Science, Vol. 2719 (July 2003), Springer: Springer Berlin), (Available as COGS Technical Report 2003:1) · Zbl 1039.68085
[19] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part I/II, J. Inform. and Comput., 100, 1-77 (1992)
[20] Milner, R.; Sangiorgi, D., Barbed bisimulation, (Kuich, W., Proc. ICALP ’92, Lecture Notes in Computer Science, Vol. 623 (1992), Springer: Springer Berlin), 685-695 · Zbl 1425.68298
[21] J.H. Morris, Lambda-calculus method of programming language, Ph.D. Thesis, MIT, December 1968.; J.H. Morris, Lambda-calculus method of programming language, Ph.D. Thesis, MIT, December 1968.
[22] Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous \(\pi \)-calculus, (Proc. POPL ’97 (January 1997), ACM: ACM New York), 256-265
[23] Phillips, I.; Vigliotti, M. G., Electoral systems in ambient calculi, (in: Proc. FoSSaCS 2004, Lecture Notes in Computer Science, Vol. 2987 (2004), Springer: Springer Berlin), 408-422 · Zbl 1126.68508
[24] Ravara, A.; Vasconelos, V. T., Typing non-uniform concurrent objects, (in: Proc. CONCUR 2000, Lecture Notes in Computer Science, Vol. 1877 (2000), Springer: Springer Berlin) · Zbl 0999.68151
[25] Sangiorgi, D., The name discipline of uniform receptiveness, Theoret. Comput. Sci., 221, 1-2, 457-493, (1999), An abstract appeared in the Proc. ICALP ’97, Lecture Notes in Computer Science, Vol. 1256, Springer, Berlin, pp. 303-313 · Zbl 0930.68035
[26] Sangiorgi, D.; Walker, D., The \(\pi \)-calculus: a Theory of Mobile Processes (2001), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0981.68116
[27] Zimmer, P., On the expressiveness of pure safe ambients, Math. Structures Comput. Sci., 13, 721-770 (2003)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.