Sound Bisimulations for Higher-Order Distributed Process Calculus
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.
- 3.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
- 4.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)Google Scholar
- 9.Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh (1992)Google Scholar
- 11.Sangiorgi, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)Google Scholar
- 12.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)Google Scholar
- 14.Schmidt, D., Dhawan, P.: Live migration with Xen virtualization software, http://www.dell.com/downloads/global/power/ps2q06-20050322-Schmidt-OE.pdf