Distributed architectures are used to improve performance and reliability of various systems. An important capability of a distributed architecture is the ability to reach consensus among all its nodes. To achieve this, several consensus algorithms have been proposed for various scenarii, and many of these algorithms come with proofs of correctness that are not mechanically checked. Unfortunately, those proofs are known to be intricate and prone to errors. In this paper, we formalize and mechanically check a consensus algorithm widely used in the distributed controls community: the Weighted-Mean Subsequence Reduced (W-MSR) algorithm proposed by Le Blanc et al. This algorithm provides a way to achieve asymptotic consensus in a distributed controls scenario in the presence of adversarial agents (attackers) that may not update their states based on the nominal consensus protocol, and may share inaccurate information with their neighbors. Using the Coq proof assistant, we formalize the necessary and sufficient conditions required to achieve resilient asymptotic consensus under the assumed attacker model. We leverage the existing Coq formalizations of graph theory, finite sets and sequences of the mathcomp library for our development. To our knowledge, this is the first mechanical proof of an asymptotic consensus algorithm. During the formalization, we clarify several imprecisions in the paper proof, including an imprecision on quantifiers in the main theorem.


翻译:使用分布式结构来提高各种系统的性能和可靠性。 分布式结构的一个重要能力是所有节点之间达成共识的能力。 为了实现这一点,已经为各种正统控制设想提出了数种共识算法, 许多这些算法都附有未经机械检查的正确性证明。 不幸的是, 这些证明已知复杂, 容易出错。 在本文中, 我们正式化并机械地检查分布式控制群体广泛使用的协商一致算法: 由勒布兰茨等人提议的加权- MEan 子序列减缩(W- MSR)算法(W- MSR)。 这个算法提供了一种方法, 在一个分布式控制设想中, 在有各种对抗性代理人(攻击者)在场的情况下, 在分布式一致协议的基础上, 提出一些可能无法更新其状态的证据。 使用 Coq 验证助理, 我们正式化了在假设攻击者模型下实现弹性性一致所需的必要和充分条件。 我们利用了现有的Coq格式化的图表理论、 定式的套件和顺序。 我们的数学缩略图库中的第一个知识, 包括机械化的校准。

0
下载
关闭预览

相关内容

专知会员服务
44+阅读 · 2020年10月31日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
【ICIG2021】Latest News & Announcements of the Workshop
中国图象图形学学会CSIG
0+阅读 · 2021年12月20日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium8
中国图象图形学学会CSIG
0+阅读 · 2021年11月16日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium4
中国图象图形学学会CSIG
0+阅读 · 2021年11月10日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium3
中国图象图形学学会CSIG
0+阅读 · 2021年11月9日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
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日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
Arxiv
0+阅读 · 2022年10月28日
VIP会员
相关VIP内容
专知会员服务
44+阅读 · 2020年10月31日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
相关资讯
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
【ICIG2021】Latest News & Announcements of the Workshop
中国图象图形学学会CSIG
0+阅读 · 2021年12月20日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium8
中国图象图形学学会CSIG
0+阅读 · 2021年11月16日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium4
中国图象图形学学会CSIG
0+阅读 · 2021年11月10日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium3
中国图象图形学学会CSIG
0+阅读 · 2021年11月9日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
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日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
Top
微信扫码咨询专知VIP会员