Sound Bisimulations for Higher-Order Distributed Process Calculus

TL;DR

This paper introduces a sound environmental bisimulation technique for higher-order π-calculus with passivation, enabling more effective reasoning about distributed systems with process transfer.

Contribution

It develops a novel environmental bisimulation method for higher-order π-calculus with passivation, improving over prior approaches that were either impractical or unsound.

Findings

Provides a sound bisimulation definition for the calculus.

Includes several non-trivial examples demonstrating applicability.

Addresses the challenge of passivation in parallel composition.

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 \emph{higher-order $\pi$-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 \emph{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.