参数化验证综述：阈值自动机与拜占庭模型检查器
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
AI总结：
本文综述了基于阈值自动机的参数化验证技术，重点介绍拜占庭模型检查器（ByMC）如何自动验证阈值守卫容错分布式算法，确保其在任意进程数和故障数下正确性。
摘要：
阈值守卫是许多容错算法的基础原语，这些算法解决分布式计算中的经典问题，如可靠广播、两阶段提交和共识。此外，阈值守卫也出现在最近的区块链算法中，例如 Tendermint 共识。本文概述了在拜占庭模型检查器（ByMC）中实现的用于阈值守卫容错分布式算法自动验证的技术。这些阈值守卫算法具有以下特征：（1）最多有 $t$ 个进程可能崩溃或表现拜占庭行为；（2）正确进程计数消息，并在收到足够多消息（例如至少 $t+1$ 条）时取得进展；（3）系统中的进程数 $n$ 是一个参数，故障数 $t$ 也是一个参数；（4）参数受弹性条件限制，例如 $n > 3t$。传统上，这些算法在最多十个参与进程的分布式系统中实现。如今，它们在涉及数百或数千个进程的分布式系统中实现。为确保这些算法在该规模下仍然正确，必须对所有可能的参数值进行验证。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
