分布式周界监视系统（DPSS）算法 A 有界收敛时间的机械化证明
计算机科学中的逻辑
2022-05-25 v1 多智能体系统
摘要
去中心化周界监视系统（DPSS）旨在提供一种去中心化协议，用于在一组无人 aerial vehicles（UAVs，无人机）之间随时间均匀分配周界监视任务，这些成员仅在彼此邻近时方可通信。该协议还必须在有界时间内收敛到周界的均匀分布。原论文中给出的两个 DPSS 协议版本似乎能在有界时间内收敛，但仅提供了非形式化证明与论证。后来对这些协议进行的模型检查应用发现其中一个关键引理存在错误，使其中一个的非形式化证明失效，并使另一个受到质疑。因此，Jeremy Avigad 和 Floris van Doorn 为较简单版本的 DPSS 协议（或称算法 A、DPSS-A）开发了新的手工收敛时间证明。本文描述了该手工证明在 ACL2 逻辑中的机械化，并讨论了三个对表达和推理 DPSS 模型特别有用的 ACL2 工具。
引用
@article{arxiv.2205.11697,
title = {A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A},
author = {David Greve and Jennifer Davis and Laura Humphrey},
journal= {arXiv preprint arXiv:2205.11697},
year = {2022}
}
备注
In Proceedings ACL2 2022, arXiv:2205.11103