Abstract
While distributed systems with transfer of processes have become pervasive, methods for reasoning about their behaviour are underdeveloped. In this paper we propose a bisimulation technique for proving behavioural equivalence of such systems modelled in the higher-order π -calculus with passivation (and restriction). Previous research for this calculus is limited to context bisimulations and normal bisimulations which are either impractical or unsound. In contrast, we provide a sound and useful definition of environmental bisimulations, with several non-trivial examples. Technically, a central point in our bisimulations is the clause for parallel composition, which must account for passivation of the spawned processes in the middle of their execution.
Appendix with full proofs at http://www.kb.ecei.tohoku.ac.jp/~adrien/pubs/SoundAppendix.pdf
Chapter PDF
Similar content being viewed by others
References
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173, 82–120 (2002)
Hewlett-Packard: Live migration across data centers and disaster tolerant virtualization architecture with HP storageworks cluster extension and Microsoft Hyper-V, http://h20195.www2.hp.com/V2/GetPDF.aspx/4AA2-6905ENW.pdf
Hildebrandt, T., Godskesen, J.C., Bundgaard, M.: Bisimulation congruences for Homer: a calculus of higher-order mobile embedded resources. Technical Report TR-2004-52, IT University of Copenhagen (2004)
Honda, K., Yoshida, N.: On reduction-based process semantics. Theoretical Computer Science 151(2), 437–486 (1995)
Howe, D.J.: Proving congruence of bisimulation in functional programming languages (1996)
Lenglet, S., Schmitt, A., Stefani, J.-B.: Normal bisimulations in calculi with passivation. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 257–271. Springer, Heidelberg (2009)
Milner, R.: Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, Cambridge (1999)
Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh (1992)
Sangiorgi, D.: Bisimulation for higher-order process calculi. Information and Computation 131, 141–178 (1996)
Sangiorgi, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science, pp. 293–302 (2007)
Sato, N., Sumii, E.: The higher-order, call-by-value applied pi-calculus. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 311–326. Springer, Heidelberg (2009)
Schmidt, D., Dhawan, P.: Live migration with Xen virtualization software, http://www.dell.com/downloads/global/power/ps2q06-20050322-Schmidt-OE.pdf
Schmitt, A., Stefani, J.-B.: The kell calculus: A family of higher-order distributed process calculi. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 146–178. Springer, Heidelberg (2005)
Sumii, E., Pierce, B.C.: A bisimulation for dynamic sealing. Theoretical Computer Science 375(1-3), 169–192 (2007); Extended abstract appeared in Proceedings of 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 161–172 (2004)
Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. Journal of the ACM 54, 1–43 (2007); Extended abstract appeared in Proceedings of 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 63–74 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Piérard, A., Sumii, E. (2011). Sound Bisimulations for Higher-Order Distributed Process Calculus. In: Hofmann, M. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2011. Lecture Notes in Computer Science, vol 6604. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19805-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-19805-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19804-5
Online ISBN: 978-3-642-19805-2
eBook Packages: Computer ScienceComputer Science (R0)