Distributed systems can be subject to various kinds of partial failures, therefore building fault-tolerance or failure mitigation mechanisms for distributed systems remains an important domain of research. In this paper, we present a calculus to formally model distributed systems subject to crash failures with recovery. The recovery model considered in the paper is weak, in the sense that it makes no assumption on the exact state in which a failed node resumes its execution, only its identity has to be distinguishable from past incarnations of itself. Our calculus is inspired in part by the Erlang programming language and in part by the distributed $\pi$-calculus with nodes and link failures (D$\pi$F) introduced by Francalanza and Hennessy. In order to reason about distributed systems with failures and recovery we develop a behavioral theory for our calculus, in the form of a contextual equivalence, and of a fully abstract coinductive characterization of this equivalence by means of a labelled transition system semantics and its associated weak bisimilarity. This result is valuable for it provides a compositional proof technique for proving or disproving contextual equivalence between systems.

翻译：分布式系统可能遭受各种类型的部分故障，因此为分布式系统构建容错或故障缓解机制仍然是一个重要的研究领域。本文提出了一种演算，用于形式化地建模遭受崩溃故障并具有恢复机制的分布式系统。本文考虑的恢复模型是弱恢复模型，其含义在于：该模型不对故障节点恢复执行时的确切状态做出任何假设，仅要求其身份能够与其自身的过往实例区分开来。我们的演算部分受到Erlang编程语言的启发，部分借鉴了Francalanza和Hennessy提出的、包含节点与链路故障的分布式π演算（DπF）。为了对具有故障和恢复机制的分布式系统进行推理，我们为演算发展了一套行为理论，其形式为上下文等价，以及通过带标签的转移系统语义及其关联的弱互模拟关系，对该等价关系给出的完全抽象的共归纳刻画。这一结果具有重要价值，因为它为证明或证否系统间的上下文等价提供了一种组合式证明技术。