Hostname: page-component-f554764f5-nt87m Total loading time: 0 Render date: 2025-04-19T05:16:49.463Z Has data issue: false hasContentIssue false
  • English
  • Français

On higher-order communication in ambient calculi

Published online by Cambridge University Press:  08 April 2025

Xian Xu Open the ORCID record for Xian Xu [Opens in a new window] ,
Yan Huang  and
Zhihuan Yao
Xian Xu*
Affiliation:
East China University of Science and Technology, Shanghai, China
Yan Huang
Affiliation:
East China University of Science and Technology, Shanghai, China
Zhihuan Yao
Affiliation:
East China University of Science and Technology, Shanghai, China
*
Corresponding author: Xian Xu; Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We revisit the communication primitive in ambient calculi. Previously, such communication was confined to first-order (FO) mode (e.g., merely names or capabilities of ambients can be sent), local mode (e.g., the communication only occurs inside an ambient), or particular cross-hierarchy mode (e.g., parent-child communication). In this work, we explore further higher-order (HO) communication in ambient calculi. Specifically, such a communication mechanism allows sending a whole piece of a program across the borders of ambients and is the only form of communication that can happen exactly between ambients. Since ambients are basically of HO nature (i.e., those being moved may be ambients themselves), in a sense, it appears more natural to have HO communication than FO communication. We stipulate that communications merely occur between equally positioned ambients in a peer-to-peer fashion (e.g., between sibling ambients). Following this line, we drop the local or other forms of communication that violate this criterion. As the workbench, we work on a variant of Fair Ambients extended with HO communication, FAHO. This variant also strengthens the original version in that entirely real-identity interaction is guaranteed. We study the semantics, bisimulation, and expressiveness of FAHO. Particularly, we provide the operational semantics using a labeled transition system. Over the semantics, we define the bisimulation in line with the standard notion of bisimulation for ambients and prove that the bisimulation equivalence (i.e., bisimilarity) is a congruence. In addition, we demonstrate that bisimilarity coincides with observational congruence (i.e., barbed congruence). Moreover, we show that FAHO can encode a minimal Turing-complete HO calculus and thus is computationally complete.

Keywords

Ambient calculuscommunicationhigher-orderprocessesencoding
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 35 , 2025 , e2
Check for updates
Copyright
© The Author(s), 2025. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable

References

Bonelli, E., Compagnoni, A., Dezani-Ciancaglini, M. and Garralda, P. (2007). Boxed ambients with communication interfaces. Mathematical Structures in Computer Science. 17 (4) 587–645.Google Scholar
Bugliesi, M., Castagna, G. and Crafa, S. (2001). Boxed ambients. In: Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001), LNCS, 38–63.CrossRefGoogle Scholar
Cao, Z. (2011). On the operational semantics of a higher order safe ambients calculus. In: Proceedings of Theoretical and Mathematical Foundations of Computer Science(ICTMF 2011), volume 164 of CCIS, 305–312,CrossRefGoogle Scholar
Cao, Z. (2012). A calculus of higher order safe ambients and its bisimulations. In: Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering (TASE 2012), 93–100.CrossRefGoogle Scholar
Cao, Z. (2013). On the expressiveness of monadic higher order safe ambient calculus. In: Proceedings of the 2013 International Conference on Foundations of Computer Science(ICTMF 2011), 305–312.Google Scholar
Cardelli, L. and Gordon, A. D. (2000). Mobile ambients. Theoretical Computer Science 240 (1) 177–213.CrossRefGoogle Scholar
Cerone, A., Hennessy, M. and Merro, M. (2012). Modelling mac-layer communications in wireless systems. In: Proceedings of the Coordination Models and Languages (COORDINATION 2013), Berlin Heidelberg: Springer, 16–30.Google Scholar
Charatonik, W., Zilio, S. D. and Gordon, A. (2003). Model checking mobile ambients. Theoretical Computer Science 308 (1-3) 277–331.CrossRefGoogle Scholar
Coppo, M. and Dezani-Ciancaglini, M. (2002). A fully abstract model for higher-order mobile ambients. In: Proceedings of the 3rd International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI 2002), volume 2294 of Lecture Notes in Computer Science, 255–271.CrossRefGoogle Scholar
Coronato, A. and Pietro, G. D. (2010). Formal design of ambient intelligence applications. Computer. 43 (12) 60–68.CrossRefGoogle Scholar
Cruz, L. R. G. and Aguirre, O. O. (2005). A virtual machine for the ambient calculus. In: Proceedings of the 2nd International Conference on Electrical and Electronics Engineering Google Scholar
Fournet, C. (1998). The Join-Calculus: a calculus for distributed mobile programming. PhD thesis, Ecole Polytechnique, Palaiseau, Nov. INRIA TU-0556. Also available from http://research.microsoft.com/∼fournet.Google Scholar
Fournet, C. and Gonthier, G. (1996). The reflexive chemical abstract machine and the join-calculus. In: Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’96), 372–385.Google Scholar
Fournet, C., Gonthier, G., Levy, J., Maranget, L. and Remy, D. (1996). A calculus of mobile agents, Proceedings of the 7th International Conference on Concurrency Theory (CONCUR ’96), volume1119 of Lecture Notes in Computer Science, 406–421.CrossRefGoogle Scholar
Fu, Y. (2005). Checking Equivalence for Higher Order Processes-a Progress Report. Technical report. BASICS lab. Shanghai Jiao Tong University, Shanghai, China.Google Scholar
Fu, Y. (2007). Fair ambients. Acta Informatica 43 (8) 535–594.CrossRefGoogle Scholar
Fu, Y. (2015). Theory of interaction. Theoretical Computer Science 611 1–49.Google Scholar
Gorla, D. (2008). Comparing communication primitives via their relative expressive power. Information and Computation 206 (8) 931–952.CrossRefGoogle Scholar
Lanese, I., Pérez, J. A., Sangiorgi, D. and Schmitt, A. (2011). On the expressiveness and decidability of higher-order process calculi. Information and Computation 209 (2) 198–226.CrossRefGoogle Scholar
Levi, F. and Sangiorgi, D. (2003). Mobile safe ambients. ACM Transactions on Programming Languages and Systems 25 (1) 1–69.CrossRefGoogle Scholar
Merro, M. and Hennessy, M. (2002). Bisimulation congruences in safe ambients. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 02), Portland, Oregon, 71–80.CrossRefGoogle Scholar
Merro, M. and Hennessy, M. (2006). A bisimulation-based semantic theory of safe ambients. ACM Transactions on Programming Languages and Systems 28 (2) 290–330.CrossRefGoogle Scholar
Milner, R. (1989). Communication and Concurrency, Prentice Hall.Google Scholar
Milner, R., Parrow, J. and Walker, D. (1992). A calculus of mobile processes (parts i and ii). Information and Computation 100 (1) 1–77.CrossRefGoogle Scholar
Mylonakis, N. (2017). A graph semantics for a variant of the ambient calculus more adequate for modeling service oriented computing. In: Electronic pre-proceedings of the Eighth International Workshop on Graph Computation Models, article 7, 1–13.Google Scholar
Pous, D. and Sangiorgi, D. (2011). Advanced Topics in Bisimulation and Coinduction, Chapter Enhancements of the Coinductive Proof Method, Cambridge University Press.Google Scholar
Sangiorgi, D. (1993). Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. Phd thesis. LFCS report ECS-LFCS-93-266. Department of Computer Science, University of Edinburgh.Google Scholar
Sangiorgi, D. (1996a). Bisimulation for higher-order process calculi. Information and Computation 131 (2) 141–178.Google Scholar
Sangiorgi, D. (1996b). Pi-calculus, internal mobility and agent-passing calculi. Theoretical Computer Science 167 (1–2) 235–274. Extracts of parts of the material contained in this paper can be found in the Proceedings of TAPSOFT’95 and ICALP’95.CrossRefGoogle Scholar
Sangiorgi, D. (2011). Introduction to Bisimulation and Coinduction, Cambridge University Press.Google Scholar
Sangiorgi, D. and Milner, R. (1992). The problem of weak bisimulation up-to. In: Proceedings of CONCUR’92, volume 630 of LNCS, Springer Verlag, 32–46.Google Scholar
Sangiorgi, D. and Rutten, J. (2012). Advanced Topics in Bisimulation and Coinduction, Cambridge University Press.Google Scholar
Sangiorgi, D. and Walker, D. (2001). The Pi-Calculus: A Theory of Mobile Processes, Cambridge University Press.Google Scholar
Schmitt, A. and Stefani, J.-B. (2003). The m-calculus: a higher-order distributed process calculus. ACM SIGPLAN Notices 38 (1) 50–61.CrossRefGoogle Scholar
Schmitt, A. and Stefani, J.-B. (2004). The Kell calculus: A family of higher-order distributed process calculi. In: Proceedings of the IST/FET International Workshop on Global Computing (GC2004), volume 3267 of Lecture Notes in Computer Science, 146–178.Google Scholar
Siewe, F., Zedan, H. and Cau, A. (2011). The calculus of context-aware ambients. Journal of Computer and System Sciences 77 (4) 597–620.CrossRefGoogle Scholar
Sun, Y. (2015). Toward a model checker for ambient logic using the process analysis toolkit. Master’s thesis, Department of Computer Science, Bishop’s University, Sherbrooke, Quebec, Canada.Google Scholar
Tomásek, M. (2007). Types for calculus of mobile code applications. Acta Electrotechnica et Informatica (7) 1–6.Google Scholar
Xu, X. (2012). Distinguishing and relating higher-order and first-order processes by expressiveness. Acta Informatica 49 (7-8) 445–484.Google Scholar