共识协议的图分析与向量分析对比
计算机科学中的逻辑
2014-07-31 v1 分布式、并行与集群计算
摘要
Paxos 分布式共识算法是标准基于向量的模型检查技术的一个具有挑战性的案例研究。由于异步通信，即使对于小型模型实例，穷尽分析也可能生成非常大的状态空间。在本文中，我们展示了图转换作为一种替代建模技术的优势。我们在一种丰富的声明式转换语言中对 Paxos 进行建模，该语言具有（除其他外）嵌套量词等特性，并使用基于图的模型检查工具 GROOVE 验证我们的模型，该工具利用同构作为通过对称性归约剪枝状态空间的自然方式。我们将结果与标准模型检查器 Spin 在基于向量的算法编码基础上获得的结果进行了比较。
引用
@article{arxiv.1407.7931,
title = {Graph- versus Vector-Based Analysis of a Consensus Protocol},
author = {Giorgio Delzanno and Arend Rensink and Riccardo Traverso},
journal= {arXiv preprint arXiv:1407.7931},
year = {2014}
}
备注
In Proceedings GRAPHITE 2014, arXiv:1407.7671