遗忘型移动机器人在 $R^2$ 中的认证通用聚集
分布式、并行与集群计算
2016-02-29 v1 数据结构与算法
计算机科学中的逻辑
机器人学
摘要
我们提出了一个统一的正式框架，用于表达移动机器人模型、协议与证明，并设计了利用该形式化框架的专用于移动机器人的协议设计/证明方法。作为一个案例研究，我们提出了首个针对在二维欧几里得空间中演化的遗忘型移动机器人的形式化认证协议。更详细地，我们为遗忘型移动机器人通用聚集问题提供了一种新算法（即：从任意非双价的初始配置开始，使用任意数量的机器人，机器人在有限步数内到达同一预先未知的位置），且不依赖于共同方向或手性。我们通过使用 COQ 证明助手形式化证明该算法正确，从而对其正确性给出了极强的保证。该结果既展示了该方法在获取尽可能少假设的新算法方面的有效性，也展示了其可管理性，因为所开发代码的数量仍保持人类可读。
引用
@article{arxiv.1602.08361,
title = {Certified Universal Gathering in $R^2$ for Oblivious Mobile Robots},
author = {Pierre Courtieu and Lionel Rieg and Sébastien Tixeuil and Xavier Urbain},
journal= {arXiv preprint arXiv:1602.08361},
year = {2016}
}
备注
arXiv admin note: substantial text overlap with arXiv:1506.01603