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模式有用。

0
下载
关闭预览

相关内容

《计算机信息》杂志发表高质量的论文,扩大了运筹学和计算的范围,寻求有关理论、方法、实验、系统和应用方面的原创研究论文、新颖的调查和教程论文,以及描述新的和有用的软件工具的论文。官网链接:https://pubsonline.informs.org/journal/ijoc
专知会员服务
123+阅读 · 2020年9月8日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium9
中国图象图形学学会CSIG
0+阅读 · 2021年12月17日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium7
中国图象图形学学会CSIG
0+阅读 · 2021年11月15日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium6
中国图象图形学学会CSIG
2+阅读 · 2021年11月12日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium5
中国图象图形学学会CSIG
1+阅读 · 2021年11月11日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium4
中国图象图形学学会CSIG
0+阅读 · 2021年11月10日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium1
中国图象图形学学会CSIG
0+阅读 · 2021年11月3日
【ICIG2021】Latest News & Announcements of the Industry Talk2
中国图象图形学学会CSIG
0+阅读 · 2021年7月29日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2022年7月12日
Arxiv
0+阅读 · 2022年7月9日
VIP会员
相关VIP内容
专知会员服务
123+阅读 · 2020年9月8日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
相关资讯
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium9
中国图象图形学学会CSIG
0+阅读 · 2021年12月17日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium7
中国图象图形学学会CSIG
0+阅读 · 2021年11月15日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium6
中国图象图形学学会CSIG
2+阅读 · 2021年11月12日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium5
中国图象图形学学会CSIG
1+阅读 · 2021年11月11日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium4
中国图象图形学学会CSIG
0+阅读 · 2021年11月10日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium1
中国图象图形学学会CSIG
0+阅读 · 2021年11月3日
【ICIG2021】Latest News & Announcements of the Industry Talk2
中国图象图形学学会CSIG
0+阅读 · 2021年7月29日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员