一句话：提出带崩溃恢复的分布式演算，并给出上下文等价的全抽象弱互模拟刻画。
分布式系统常遭遇各类部分失效，构建容错与失效缓解机制是重要研究方向。本文提出一个演算，用于形式化建模带崩溃失效与恢复的分布式系统。其恢复模型是“弱”的：不假设失效节点恢复时的具体状态，只要求其身份能与自身过往化身区分。演算部分受 Erlang 语言启发，并借鉴 Francalanza 与 Hennessy 的带节点和链路失效的分布式 π 演算 DπF。为推理此类系统，作者建立了行为理论，包括上下文等价，以及基于标号迁移系统语义和弱互模拟的全抽象余归纳刻画。该结果提供了证明或证否系统间上下文等价的组合式证明技术。
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 $π$-calculus with nodes and link failures (D$π$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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FabbrettiLS25,
title = {A Behavioral Theory for Distributed Systems with Weak Recovery},
author = {Giovanni Fabbretti and Ivan Lanese and Jean-Bernard Stefani},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:1)2025}
}