{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T17:55:25Z","timestamp":1743098125309,"version":"3.40.3"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572456"},{"type":"electronic","value":"9783031572463"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T00:00:00Z","timestamp":1712188800000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Distributed architectures are used to improve performance and reliability of various systems. Examples include drone swarms and load-balancing servers. An important capability of a distributed architecture is the ability to reach consensus among all its nodes. Several consensus algorithms have been proposed, and many of these algorithms come with intricate proofs of correctness, that are not mechanically checked. In the controls community, algorithms often achieve consensus<jats:italic>asymptotically<\/jats:italic>, e.g., for problems such as the design of human control systems, or the analysis of natural systems like bird flocking. This is in contrast to exact consensus algorithm such as Paxos, which have received much more recent attention in the formal methods community.<\/jats:p><jats:p>This paper presents the first formal proof of an asymptotic consensus algorithm, and addresses various challenges in its formalization. Using the Coq proof assistant, we verify the correctness of a widely used consensus algorithm in the distributed controls community, the<jats:italic>Weighted-Mean Subsequence Reduced (W-MSR) algorithm<\/jats:italic>. We formalize the necessary and sufficient conditions required to achieve resilient asymptotic consensus under the assumed attacker model. During the formalization, we clarify several imprecisions in the paper proof, including an imprecision on quantifiers in the main theorem.<\/jats:p>","DOI":"10.1007\/978-3-031-57246-3_14","type":"book-chapter","created":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T14:03:43Z","timestamp":1712153023000},"page":"248-267","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formally verified asymptotic consensus in robust networks"],"prefix":"10.1007","author":[{"given":"Mohit","family":"Tekriwal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Avi","family":"Tachna-Fram","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Baptiste","family":"Jeannin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manos","family":"Kapritsos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dimitra","family":"Panagou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,4]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Cohen, C.: Formal foundations of 3d geometry to model robot manipulators. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. pp. 30\u201342 (2017).","DOI":"10.1145\/3018610.3018629"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Althoff, M., Krogh, B.H.: Zonotope bundles for the efficient computation of reachable sets. In: 2011 50th IEEE conference on decision and control and European control conference. pp. 6814\u20136821. IEEE (2011).","DOI":"10.1109\/CDC.2011.6160872"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Araiza-Illan, D., Eder, K., Richards, A.: Formal verification of control systems\u2019 properties with theorem proving. In: 2014 UKACC International Conference on Control (CONTROL). pp. 244\u2013249. IEEE (2014).","DOI":"10.1109\/CONTROL.2014.6915147"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: International Workshop on Hybrid Systems: Computation and Control. pp. 73\u201388. Springer (2000).","DOI":"10.1007\/3-540-46430-1_10"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Carr, H., Jenkins, C., Moir, M., Miraldo, V.C., Silva, L.: Towards formal verification of hotstuff-based byzantine fault tolerant consensus in agda. In: NASA Formal Methods Symposium. pp. 616\u2013635. Springer (2022).","DOI":"10.1007\/978-3-031-06773-0_33"},{"key":"14_CR6","unstructured":"Castro, M., Liskov, B., et\u00a0al.: Practical byzantine fault tolerance.In: OSDI.vol.\u00a099, pp. 173\u2013186 (1999)"},{"key":"14_CR7","unstructured":"Chan, M., Ricketts, D., Lerner, S., Malecha, G.: Formal verification of stability properties of cyber-physical systems. Proc. CoqPL (2016)"},{"key":"14_CR8","unstructured":"Charron-Bost, B., Merz, S.: Formal verification of a consensus algorithm in theheard-of model. Int. J. Softw. Informatics 3(2-3), 273\u2013303 (2009)"},{"key":"14_CR9","unstructured":"Charron-Bost, B., Merz, S.: Formal Verification of a Consensus Algorithm in the Heard-Of Model. International Journal of Software and Informatics (IJSI) 3(2\u20133), 273\u2013303 (2009), https:\/\/inria.hal.science\/inria-00426388."},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Chutinan, A., Krogh, B.H.: Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: International workshop on hybrid systems: computation and control. pp. 76\u201390. Springer (1999).","DOI":"10.1007\/3-540-48983-5_10"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli,F., Traverso, P.: Formal verification of a railway interlocking system using model checking. Formal aspects of computing 10(4), 361\u2013380 (1998)","DOI":"10.1007\/s001650050022"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Cohen, C., Rouhling, D.: A formal proof in coq of lasalle\u2019s invariance principle. In: International Conference on Interactive Theorem Proving. pp. 148\u2013163. Springer (2017).","DOI":"10.1007\/978-3-319-66107-0_10"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Doczkal, C., Pous, D.: Graph theory in coq: Minors, treewidth, and isomorphisms. Journal of Automated Reasoning 64(5), 795\u2013825 (2020)","DOI":"10.1007\/s10817-020-09543-2"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Farahani, S.S., Raman, V., Murray, R.M.: Robust model predictive control for signal temporal logic synthesis. IFAC-PapersOnLine 48(27), 323\u2013328 (2015)","DOI":"10.1016\/j.ifacol.2015.11.195"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3-where programs meet provers. In: European symposium on programming. pp. 125\u2013128. Springer (2013).","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"F\u00fcgger, M., Nowak, T., Schwarz, M.: Tight bounds for asymptotic and approximate consensus. Journal of the ACM (JACM) 68(6), 1\u201335 (2021)","DOI":"10.1145\/3485242"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Gallois-Wong, D., Boldo, S., Hilaire, T.: A coq formalization of digital filters. In: International Conference on Intelligent Computer Mathematics. pp. 87\u2013103. Springer (2018).","DOI":"10.1007\/978-3-319-96812-4_8"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Gao, S., Zhan, B., Liu, D., Sun, X., Zhi, Y., Jansen, D.N., Zhang, L.: Formal verification of consensus in the taurus distributed database. In: Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20\u201326, 2021, Proceedings 24. pp. 741\u2013751. Springer (2021).","DOI":"10.1007\/978-3-030-90870-6_42"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Girard, A., Guernic, C.L.: Zonotope\/hyperplane intersection for hybrid systems reachability analysis. In: International Workshop on Hybrid Systems: Computation and Control. pp. 215\u2013228. Springer (2008).","DOI":"10.1007\/978-3-540-78929-1_16"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Goel, A., Sakallah, K.: On symmetry and quantification: A new approach to verify distributed protocols. In: NASA Formal Methods Symposium. pp. 131\u2013150. Springer (2021).","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"14_CR21","unstructured":"Hance, T., Heule, M., Martins, R., Parno, B.: Finding invariants of distributed systems: It\u2019s a small (enough) world after all. In: 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). pp. 115\u2013131 (2021)."},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Hol light: A tutorial introduction. In: International Conference on Formal Methods in Computer-Aided Design. pp. 265\u2013269. Springer (1996).","DOI":"10.1007\/BFb0031814"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Hasan, O., Ahmad, M.: Formal analysis of steady state errors in feedback control systems using hol-light. In: 2013 Design, Automation & Test in Europe Conference & Exhibition (DATE). pp. 1423\u20131426. IEEE (2013).","DOI":"10.7873\/DATE.2013.290"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Havelund, K., Pressburger, T.: Model checking java programs using javapathfinder. International Journal on Software Tools for Technology Transfer2(4), 366\u2013381 (2000)","DOI":"10.1007\/s100090050043"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B.,Roberts, M.L., Setty, S., Zill, B.: Ironfleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles. pp. 1\u201317 (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Jasim, O.A., Veres, S.M.: Towards formal proofs of feedback control theory. In: 2017 21st International Conference on System Theory, Control and Computing (ICSTCC). pp. 43\u201348. IEEE (2017).","DOI":"10.1109\/ICSTCC.2017.8107009"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Kieckhafer, R.M., Azadmanesh, M.H.: Reaching approximate agreementwith mixed-mode faults. IEEE Transactions on Parallel and Distributed Systems 5(1), 53\u201363 (1994)","DOI":"10.1109\/71.262588"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Kochdumper, N., Althoff, M.: Sparse polynomial zonotopes: A novelset representation for reachability analysis. IEEE Transactions on Automatic Control 66(9), 4043\u20134058 (2020)","DOI":"10.1109\/TAC.2020.3024348"},{"key":"14_CR29","unstructured":"Lamport, L., et\u00a0al.: Paxos made simple. ACM Sigact News 32(4), 18\u201325 (2001)"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"LeBlanc, H.J., Zhang, H., Koutsoukos, X., Sundaram, S.: Resilient asymptotic consensus in robust networks. IEEE Journal on Selected Areas in Communications 31(4), 766\u2013781 (2013)","DOI":"10.1109\/JSAC.2013.130413"},{"key":"14_CR31","unstructured":"Losa, G., Dodds, M.: On the formal verification of the stellar consensus protocol. In: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2020)."},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Lozano, R., Fantoni, I., Block, D.J.: Stabilization of the inverted pendulum around its homoclinic orbit. Systems & control letters 40(3), 197\u2013204 (2000)","DOI":"10.1016\/S0167-6911(00)00025-6"},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"Ma, H., Goel, A., Jeannin, J.B., Kapritsos, M., Kasikci, B., Sakallah, K.A.: I4: incremental inference of inductive invariants for verification of distributed protocols. In: Proceedings of the 27th ACM Symposium on Operating Systems Principles. pp. 370\u2013384 (2019).","DOI":"10.1145\/3341301.3359651"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Mesbahi, M., Egerstedt, M.: Graph theoretic methods in multiagent networks. Princeton University Press (2010).","DOI":"10.1515\/9781400835355"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Moon, I., Powers, G.J., Burch, J.R., Clarke, E.M.: Automatic verification of sequential control systems using temporal logic. AIChE Journal 38(1), 67\u201375 (1992)","DOI":"10.1002\/aic.690380107"},{"key":"14_CR36","unstructured":"Ongaro, D., Ousterhout, J.: In search of an understandable consensus algorithm. In: 2014 $$\\{$$USENIX$$\\}$$ Annual Technical Conference ($$\\{$$USENIX$$\\}$$$$\\{$$ATC$$\\}$$ 14). pp. 305\u2013319 (2014)."},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Isabelle: A generic theorem prover. Springer (1994).","DOI":"10.1007\/BFb0030541"},{"key":"14_CR38","doi-asserted-by":"crossref","unstructured":"Rashid, A., Hasan, O.: Formalization of transform methods using hol light. In: International Conference on Intelligent Computer Mathematics. pp. 319\u2013332. Springer (2017).","DOI":"10.1007\/978-3-319-62075-6_22"},{"key":"14_CR39","doi-asserted-by":"crossref","unstructured":"Rouhling, D.: A formal proof in coq of a control function for the inverted pendulum. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 28\u201341 (2018).","DOI":"10.1145\/3167101"},{"key":"14_CR40","doi-asserted-by":"crossref","unstructured":"Sadraddini, S., Belta, C.: Robust temporal logic model predictive control. In: 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton). pp. 772\u2013779. IEEE (2015).","DOI":"10.1109\/ALLERTON.2015.7447084"},{"key":"14_CR41","doi-asserted-by":"crossref","unstructured":"Saldana, D., Prorok, A., Sundaram, S., Campos, M.F., Kumar, V.: Resilient consensus for time-varying networks of dynamic agents. In: 2017 American control conference (ACC). pp. 252\u2013258. IEEE (2017).","DOI":"10.23919\/ACC.2017.7962962"},{"key":"14_CR42","doi-asserted-by":"crossref","unstructured":"Saulnier, K., Saldana, D., Prorok, A., Pappas, G.J., Kumar, V.:Resilientflocking for mobile robot teams. IEEE Robotics and Automation letters2(2), 1039\u20131046 (2017)","DOI":"10.1109\/LRA.2017.2655142"},{"key":"14_CR43","unstructured":"Scherer, S., Lerda, F., Clarke, E.M.: Model checking of robotic control systems (2005)."},{"key":"14_CR44","doi-asserted-by":"publisher","unstructured":"Schneider, F.B.: Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Comput. Surv. 22(4), 299\u2013319 (dec 1990). https:\/\/doi.org\/10.1145\/98163.98167,https:\/\/doi.org\/10.1145\/98163.98167.","DOI":"10.1145\/98163.98167 10.1145\/98163.98167"},{"key":"14_CR45","unstructured":"Tekriwal, M., Tachna-Fram, A., Jeannin, J.B., Kapritsos, M., Panagou, D.: Formally verified asymptotic consensus in robust networks (extended version). arXiv preprint arXiv:2202.13833 (2022)."},{"key":"14_CR46","doi-asserted-by":"publisher","unstructured":"Usevitch, J., Garg, K., Panagou, D.: Finite-time resilient formation control with bounded inputs. In: 2018 IEEE Conference on Decision and Control (CDC). pp. 2567\u20132574. IEEE (2018). https:\/\/doi.org\/10.1109\/CDC.2018.8619697","DOI":"10.1109\/CDC.2018.8619697"},{"key":"14_CR47","doi-asserted-by":"crossref","unstructured":"Van\u00a0Renesse, R., Altinbuken, D.: Paxos made moderately complex. ACM ComputingSurveys (CSUR) 47(3), 1\u201336 (2015)","DOI":"10.1145\/2673577"},{"key":"14_CR48","doi-asserted-by":"crossref","unstructured":"Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.: Verdi: a framework for implementing and formally verifying distributed systems. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 357\u2013368 (2015).","DOI":"10.1145\/2737924.2737958"},{"key":"14_CR49","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J., Jana, S., Ryan, G.: DistAI: Data-driven automated invariant learning for distributed protocols. In: 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). pp. 405\u2013421 (2021)."},{"key":"14_CR50","doi-asserted-by":"crossref","unstructured":"Zhang, H., Sundaram, S.: Robustness of information diffusion algorithms to locally bounded adversaries. In: 2012 American Control Conference (ACC). pp. 5855\u20135861. IEEE (2012).","DOI":"10.1109\/ACC.2012.6315661"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57246-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T16:15:11Z","timestamp":1731687311000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57246-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572456","9783031572463"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57246-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"4 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}