论文标题
分布式外围监视系统（DPSS）算法A的机械化证明
A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A
论文作者
论文摘要
分散的外围监视系统（DPSS）试图提供一项分散的方案，以均匀地分配随着时间的流逝，对无人驾驶汽车（无人机）（无人机）进行监视，其成员只有在与彼此近距离接近时才进行交流。 该协议还必须在有限的时间内收敛到周长的均匀分布。 原始论文中介绍的DPSS协议的两个版本似乎在有限的时间内收敛，但仅给出非正式的证据和参数。 后来的模型检查对这些协议的应用程序发现了一个关键引理之一中的错误，使一个非正式的证据无效，并对另一个进行了怀疑。 因此，杰里米·阿维加德（Jeremy Avigad）和弗洛里斯·范·杜恩（Floris Van Doorn）开发了简单版本或算法Algorithm A或DPSS-A算法AlgorithM A或DPSS-A的收敛时间的新手动证明。本文描述了ACL2逻辑中该手动证明的机械化，并讨论了三个特定的ACL2实用程序，这些实用程序证明对DPSS模型表达和推理很有用。
The decentralized perimeter surveillance system (DPSS) seeks to provide a decentralized protocol for evenly distributing surveillance of a perimeter over time across an ensemble of unmanned aerial vehicles (UAVs) whose members may communicate only when in close proximity to each other. The protocol must also converge to an even distribution of the perimeter in bounded time. Two versions of the DPSS protocol presented in the original paper seem to converge in bounded time but only informal proofs and arguments are given. A later application of model checking to these protocols found an error in one of the key lemmas, invalidating the informal proof for one and casting doubt on the other. Therefore, a new hand proof of the convergence time for the simpler version of the DPSS protocol or algorithm, Algorithm A or DPSS-A, was developed by Jeremy Avigad and Floris van Doorn. This paper describes a mechanization of that hand proof in the logic of ACL2 and discusses three specific ACL2 utilities that proved useful for expressing and reasoning about the DPSS model.
