Location and link failure in a distributed π-calculus

Abstract

We develop a behavioural theory of distributed systems in the presence of failures. The framework we use is that of Dπ, a language in which located processes, or agents, may migrate between dynamically created locations. These processes run on a distributed network, in which individual nodes may fail, or the links between them may be broken. The original language, Dπ, is extended by a new construct for detecting and reacting to these failures together with constructs that induce failure. We define a bisimulation equivalence between these systems, based on labelled actions which record, in addition to the effect actions have on the processes, the actual state of the underlying network and the view of this state known to observers. We prove that the equivalence is fully abstract, in the sense that two systems will be differentiated if and only if, in some sense, there is a computational context, consisting of a network and an observer, which can see the difference.