一句话：将容错机制引入多方会话类型，支持不可靠通信与进程崩溃，并用失败模式增强进程语义以分析分布式算法。
多方会话类型用于抽象通信协议结构并验证行为属性，其中 progress（无死锁）尤为重要。分布式算法常可视为多方通信协议，但其终止性等属性证明复杂，且算法常需应对故障。本文把容错集成进多方会话类型，使其能处理不可靠通信和进程崩溃；同时扩展进程语义，引入失败模式（failure patterns）以刻画系统需求，例如故障检测器。作者以 Chandra 和 Toueg 的 rotating coordinator 算法的一个变体为案例，说明如何用该框架分析和验证容错分布式算法。该工作为用会话类型验证分布式算法迈出一步。
Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often resemble multiparty communication protocols. But proving their properties, in particular termination that is closely related to progress, can be elaborate. Since distributed algorithms are often designed to cope with faults, a first step towards using session types to verify distributed algorithms is to integrate fault-tolerance. We extend multiparty session types to cope with system failures such as unreliable communication and process crashes. Moreover, we augment the semantics of processes by failure patterns that can be used to represent system requirements (as, e.g., failure detectors). To illustrate our approach we analyse a variant of the well-known rotating coordinator algorithm by Chandra and Toueg.
@article{paperbot2180,
title = {FTMPST: Fault-Tolerant Multiparty Session Types},
author = {Kirstin Peters and Uwe Nestmann and Christoph Wagner},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:14)2023}
}