Sound Bisimulations for Higher-Order Distributed Process Calculus

Abstract. While distributed systems with transfer of processes have become pervasive, methods for reasoning about their behaviour are underdeveloped. In this paper we develop 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 useful, sound and complete 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.

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Adrien Piérard, Eijiro Sumii
• Keywords: Behavioural Equivalence, Bisimulation Technique, CORR 2010, Distributed Systems, Education