容错移动机器人的认证不可能性结果
计算机科学中的逻辑
2013-06-19 v1 分布式、并行与集群计算
摘要
我们提出了一个使用 COQ 证明助手构建机器人网络形式化开发的框架，用于形式化地陈述和证明各种性质。本文聚焦于不可能性证明，因为利用 COQ 的高阶演算将算法作为抽象对象进行推理是很自然的。我们特别展示了关于无记忆移动机器人收敛性的两个不可能性结果的形式化证明：当分别超过一半和超过三分之一的机器人表现出拜占庭故障时，这些证明基于 Bouzid 等人提出的原始定理。得益于我们的形式化工作，相应的 COQ 开发相当紧凑。据我们所知，这是机器人网络领域首批经过认证（即形式化证明）的不可能性结果。
引用
@article{arxiv.1306.4242,
title = {Certified Impossibility Results for Byzantine-Tolerant Mobile Robots},
author = {Cédric Auger and Zohir Bouzid and Pierre Courtieu and Sébastien Tixeuil and Xavier Urbain},
journal= {arXiv preprint arXiv:1306.4242},
year = {2013}
}