.png){kind=icon}
返回
Verifying Almost-Sure Termination for Randomized Distributed Algorithms
.png){kind=icon}
PRE
AI
DOI：10.1145/3776691.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
我们提出了一种用于验证随机分布式算法活性属性的技 术。我们的技术为许多常见的共识算法提供了基于SMT的证明，无论是针对崩溃故障还是拜占庭故障。它基于分布式系统公平几乎必然终止的一个可靠的证明规则，该规则结合了基于鞅的几乎必然终止技术与关于弱公平性的推理。我们的证明规则能够处理参数化协议，其中状态无界增长且每个变体函数无界。这些协议超出了先前方法的研究范围，因为先前方法要么依赖有界变体函数，要么依赖归约到（非概率）公平性。我们在Caesar（一个概率程序验证器）上实现了我们的证明规则。我们使用该证明规则为随机异步共识协议的终止属性提供基于SMT的证明，包括Ben-Or协议和分级二进制共识，针对崩溃和拜占庭故障均适用。这些协议的终止证明历来十分困难，但均属于我们证明规则的研究范围。
Keyword:
probabilistic programs
proof rules
almost-sure termination
期刊
P
IF:
2.8
论文数:
308
被引数:
4.7K
机构
引用论文
.png){kind=icon}
Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
PREAI
分享收藏分享收藏
查看更多内容