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.
翻译:分散式周边监视系统(DPSS)试图提供一种分散式协议,以便随着时间的推移在一组无人驾驶飞行器(无人驾驶飞行器)之间平均分配对周边的监视,无人驾驶飞行器的成员只有在彼此关系密切时才能进行交流;议定书还必须在交界时间达到周界的均衡分布;原始文件中提供的DPSS议定书的两种版本似乎在受约束的时间里趋同,但只提供了非正式证据和论据;后来对这些议定书进行示范检查时发现其中一种在关键轴中有一个错误,使其中一种非正式证据无效,并引起怀疑;因此,Jeremy Avigad和Floris van Dourn开发了一个新的手证统一时间的新手证,证明对简化版DPSS协议或算法Algorithm A或DPSS-A的趋同时间,这是Jeremy Avorigad和Floris van Dourn开发的,该文件在ACL2逻辑中描述了手证的机械化,并讨论了三套具体的ACL2公用事业,证明对表达和解释DPSS模式有用。