弱对手下随机分布式算法的约简定理

### 弱对手下随机分布式算法的约简定理 #### 1. 引言 自动化验证容错分布式算法面临组合爆炸问题，因为许多进程的异步并行组合会产生大量执行情况。近期一些验证方法提出，对于许多分布式算法，考虑较少的（代表性）同步执行就足够了。其核心思路是通过反复交换相邻转换，将任意执行转换为代表性的同步执行，这种方法适用于可达性属性和特定的无抖动线性时态属性。 本文将这一思想扩展到随机分布式算法和概率属性。概率保证需要在马尔可夫决策过程（MDP）中进行推理，MDP 中的非确定性通过对手（adversaries）来解决，对手是将执行前缀映射到下一个动作的函数。当遇到抛硬币动作时，会产生分支，每个分支都关联一个概率，MDP 和对手共同诱导出一个具有概率分支的计算树。 在分布式共识算法分析中，有两类研究较多的对手：强对手和弱对手。强对手对执行前缀有完全的了解，而弱对手基于执行前缀的投影（抽象），特别是它们无法访问交换消息的内容和抛硬币的结果。本文对弱对手进行了形式化，并明确指出它们对分布式算法的本地代码有内在限制，即只能为一类分布式算法定义弱对手。 直观上，这些算法在本地控制流方面表现出某种对称性。例如 Ben - Or 的共识算法，其控制流在 0 侧和 1 侧是对称的；而一些不对称的示例中，对手可能会推断出关于共识值的信息。典型的随机共识算法通常具有类似 Ben - Or 算法的对称结构，其几乎确定终止性已在同步执行（通过轮次刚性对手形式化）下得到自动验证。本文将证明，对于这些分布式算法，由弱对手定义的计算树可以通过交换论证简化为轮次刚性计算树。 #### 2. 随机阈值算法建模 概率阈值自动机（Probabilistic Threshold Automaton with Processes，PTAP）是一个元组 (L, Z, R, RC)，各部分定义如下： - **L**：非空有限位置集，包含初始位置 I、最终位置 F 和边界位置 B，且 |B| = |I|。 - **Z**：由以下五个集合的不相交并集组成： - **Π**：参数变量集。 - **P**：有限进程集，是正确进程集 C 和故障进程集 F 的不相交并集。 - **T**：消息类型的有限集。 - **V**：消息值的有限集，通常 V = {0, 1}。 - **Λ**：本地接收变量集，Λ ⊆ {xt,v | t ∈ T, v ∈ V}。 - **R**：有限规则集。 - **RC**：弹性条件，是对参数变量的约束。 以 Ben - Or 的随机共识算法为例，其 PTAP 有特定的规则和位置。规则用于描述进程的行为，例如发送消息、根据接收到的消息数量进行状态转换等。随机化通过规则 r10 引入，这是一个抛硬币动作，进程根据结果选择下一轮的估计值。 ##### 2.1 PTAP 的对称性 在 PTAP 模型中，为了形式化弱对手，引入了两个等价关系： - **规则和守卫的等价关系**： - 简单阈值守卫 ϕ1 和 ϕ2 对应，如果它们的关系运算符相同、系数相同、消息类型相同，并且存在值集 V 上的置换 π 使得系数对应相等。 - 规则 r1 和 r2 等价，如果它们的守卫对应且存在值集 V 上的置换 π 使得更新集对应。 - **位置的等价关系**： - 边界位置 B 是一个等价类。 - 对于 L \ B 中的两个位置 ℓ1 和 ℓ2，如果存在规则 r1 和 r2 以及源位置 ℓs1 和 ℓs2，满足源位置等价、规则等价且 ℓ1 和 ℓ2 分别是 r1 和 r2 的目标位置，则 ℓ1 和 ℓ2 等价。 - 最终位置 F 要么是一个等价类，要么是有限个等价类的并集。 例如，在 Ben - Or 算法的 PTAP 中，有 7 个关于位置等价关系的等价类。而一些不对称的自动机无法定义位置的等价关系，因为对手可能会推断出消息内容或抛硬币结果的信息。 ##### 2.2 PTAP 的语义 PTAP 的语义是一个无限状态的马尔可夫决策过程（MDP），记为 Sys(PTAP) = (Σ, I, Act, Δ)，其中： - **Σ**：配置集，配置 σ 是一个元组 (s, Sent, Rcvd, p)，分别描述进程的控制状态、已发送的消息集、每个进程接收到的消息集和参数值。 - **I**：初始配置集，初始配置中所有进程位于边界位置，且没有发送或接收任何消息。 - **Act**：动作集，动作 α = (M, p) 表示进程 p 接收消息集 M 并尝试执行规则。 - **Δ**：概率转移函数，定义了从一个配置到另一个配置的转移概率。 路径是配置和动作的交替序列，有限路径的长度是动作的数量。在路径上，已发送的消息集只会增加。 #####