一句话：综述用阈值自动机和 ByMC 对阈值守卫容错分布式算法进行参数化自动验证的技术。
本文综述面向阈值守卫容错分布式算法的自动化验证技术，以及这些技术在 Byzantine Model Checker（ByMC）中的实现。此类算法允许至多 t 个进程崩溃或表现拜占庭行为；正确进程通过计数消息并在收到足够多消息（如至少 t+1 条）时推进；进程数 n 与故障数 t 均为参数，并受 n > 3t 等弹性条件约束。由于现代分布式系统可包含数百乃至数千进程，必须对所有满足条件的参数取值验证算法正确性。文章介绍阈值自动机等参数化验证方法，并覆盖可靠广播、两阶段提交、共识以及 Tendermint 等经典与区块链算法。
Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems in distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent blockchain algorithms such as, e.g., Tendermint consensus. In this article, we give an overview of techniques for automated verification of threshold-guarded fault-tolerant distributed algorithms, implemented in the Byzantine Model Checker (ByMC). These threshold-guarded algorithms have the following features: (1) up to $t$ of processes may crash or behave Byzantine; (2) the correct processes count messages and make progress when they receive sufficiently many messages, e.g., at least $t+1$; (3) the number $n$ of processes in the system is a parameter, as well as the number $t$ of faults; and (4) the parameters are restricted by a resilience condition, e.g., $n > 3t$. Traditionally, these algorithms were implemented in distributed systems with up to ten participating processes. Nowadays, they are implemented in distributed systems that involve hundreds or thousands of processes. To make sure that these algorithms are still correct for that scale, it is imperative to verify them for all possible values of the parameters.
@article{paperbot2243,
title = {Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker},
author = {Igor Konnov and Marijana Lazić and Ilina Stoilkovska and Josef Widder},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:5)2023}
}