Document Open Access Logo

Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems

Authors Nathalie Bertrand , Pranav Ghorpade , Sasha Rubin

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.20.pdf
  • Filesize: 1.08 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Distributed algorithms
Keywords
  • parametrized verification
  • asynchronous round-based distributed algorithms
  • finite-counter systems
  • LTL model checking

Metrics

Abstract

Traditional model-checking techniques typically verify distributed algorithms only for a fixed number of finite-state processes. Parameterized model checking generalizes this to any number of processes, while still typically assuming that each process is finite-state. In this work, we consider asynchronous round-based distributed algorithms in which each process is infinite-state since it can execute for an infinite number of rounds. We show that the parameterized verification problem for asynchronous round-based distributed algorithms is undecidable, already for simple specifications. Nevertheless, as our main contribution, we provide a reduction to LTL model checking over finite-counter systems and prove that it is sound and complete. This enables the use of off-the-shelf, mature symbolic model checkers for finite-counter systems. We demonstrate the practical applicability of this reduction by verifying safety and liveness properties of several asynchronous round-based consensus and leader-election algorithms using the nuXmv model checker.

Cite As Get BibTex

Nathalie Bertrand, Pranav Ghorpade, and Sasha Rubin. Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 20:1-20:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.20

Author Details

Nathalie Bertrand
  • Univ Rennes, Inria, CNRS, IRISA, France
Pranav Ghorpade
  • The University of Sydney, Australia
Sasha Rubin
  • The University of Sydney, Australia

Funding

  • Bertrand, Nathalie: Projects ANR BisoUS (ANR-22-CE48-0012) and ANR PaVeDyS (ANR-23-CE48-0005).
  • Ghorpade, Pranav: Supported by University of Sydney Faculty of Engineering Research Scholarship.

References

  1. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  2. Leemon Baird and Atul Luykx. The hashgraph protocol: Efficient asynchronous BFT for high-throughput distributed ledgers. In Proceedings of the 2020 International Conference on Omni-layer Intelligent Systems (COINS 2020), pages 1-7. IEEE, 2020. URL: https://doi.org/10.1109/COINS49042.2020.9191430.
  3. Michael Ben-Or. Another advantage of free choice (extended abstract): Completely asynchronous agreement protocols. In Procedings of the 2nd Annual ACM Symposium on Principles of Distributed Computing (PODC 1983), pages 27-30. Association for Computing Machinery, 1983. URL: https://doi.org/10.1145/800221.806707.
  4. Nathalie Bertrand, Pranav Ghorpade, and Sasha Rubin. Parameterized verification of asynchronous round-based distributed algorithms via reduction to finite-counter systems, 2026. URL: https://arxiv.org/abs/2606.27867.
  5. Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin, Bernhard Scholz, and Pavle Subotić. Reusable formal verification of dag-based consensus protocols. In Proceedings of the 17th International Symposium on NASA Formal Methods (NFM 2025), pages 138-158. Springer-Verlag, 2025. URL: https://doi.org/10.1007/978-3-031-93706-4_9.
  6. Nathalie Bertrand, Igor Konnov, Marijana Lazić, and Josef Widder. Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In Proceedings of the 30th International Conference on Concurrency Theory (CONCUR 2019), volume 140 of Leibniz International Proceedings in Informatics (LIPIcs), pages 33:1-33:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.33.
  7. Nathalie Bertrand, Bastien Thomas, and Josef Widder. Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms. In Proceeding of the 32nd International Conference on Concurrency Theory (CONCUR 2021), volume 203 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.15.
  8. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. URL: https://doi.org/10.2200/S00658ED1V01Y201508DCT013.
  9. Gabriel Bracha. Asynchronous Byzantine agreement protocols. Information and Computation, 75(2):130-143, 1987. URL: https://doi.org/10.1016/0890-5401(87)90054-X.
  10. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuXmv symbolic model checker. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV 2014), pages 334-342. Springer International Publishing, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_22.
  11. Saksham Chand, Yanhong A. Liu, and Scott D. Stoller. Formal verification of multi-paxos for distributed consensus. In Proceedings of the 21st International Symposium on Formal Methods (FM 2016), volume 9995 of Lecture Notes in Computer Science, pages 119-136, 2016. URL: https://doi.org/10.1007/978-3-319-48989-6_8.
  12. Tushar Deepak Chandra and Sam Toueg. Unreliable failure detectors for reliable distributed systems. J. ACM, 43(2):225-267, March 1996. URL: https://doi.org/10.1145/226643.226647.
  13. Mouna Chaouch-Saad, Bernadette Charron-Bost, and Stephan Merz. A reduction theorem for the verification of round-based distributed algorithms. In Proceedings of the 3rd International Workshop on Reachability Problems (RP 2009), pages 93-106. Springer Berlin Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-04420-5_10.
  14. Bernadette Charron-Bost and André Schiper. The heard-of model: computing in distributed systems with benign faults. Distributed Computing, 22(1):49-71, April 2009. URL: https://doi.org/10.1007/s00446-009-0084-6.
  15. Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A storm is coming: A modern probabilistic model checker, 2017. URL: https://arxiv.org/abs/1702.04311.
  16. Giorgio Delzanno, Michele Tatarek, and Riccardo Traverso. Model checking paxos in spin. In Proceedings 5th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2014), volume 161 of EPTCS, pages 131-146, 2014. URL: https://doi.org/10.4204/EPTCS.161.13.
  17. Stéphane Demri, Alain Finkel, Valentin Goranko, and Govert van Drimmelen. Model-checking ctl* over flat presburger counter systems. J. Appl. Non Class. Logics, 20(4):313-344, 2010. URL: https://doi.org/10.3166/JANCL.20.313-344.
  18. Fantom Foundation. Lachesis aBFT, 2024. URL: https://docs.fantom.foundation/technology/lachesis-abft.
  19. Adam Gagol, Damian Lesniak, Damian Straszak, and Michal Swietek. Aleph: Efficient atomic broadcast in asynchronous networks with Byzantine nodes. In Proceedings of the 1st ACM Conference on Advances in Financial Technologies (AFT 2019), pages 214-228. ACM, 2019. URL: https://doi.org/10.1145/3318041.3355467.
  20. Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675-735, 1992. URL: https://doi.org/10.1145/146637.146681.
  21. Pranav Ghorpade. Github case studies repository, 2026. URL: https://github.com/pranavg5526/Parameterized-Verification-of-Round-Based-Distributed-Algorithms.
  22. Aman Goel and Karem Sakallah. On symmetry and quantification: A new approach to verify distributed protocols. In Proceedings of the 13th International Symposium on NASA Formal Methods (NFM 2021), pages 131-150, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-76384-8_9.
  23. Idit Keidar, Eleftherios Kokoris-Kogias, Oded Naor, and Alexander Spiegelman. All you need is DAG. In Proceedings of 40th ACM Symposium on Principles of Distributed Computing (PODC 2021), pages 165-175. ACM, 2021. URL: https://doi.org/10.1145/3465084.3467905.
  24. Idit Keidar, Oded Naor, Ouri Poupko, and Ehud Shapiro. Cordial miners: Fast and efficient consensus for every eventuality. In Proceedings of the 37th International Symposium on Distributed Computing, (DISC 2023), volume 281 of LIPIcs, pages 26:1-26:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.DISC.2023.26.
  25. Jason R. Koenig, Oded Padon, Sharon Shoham, and Alex Aiken. Inferring invariants with quantifier alternations: Taming the search space explosion. In TACAS (1), volume 13243 of Lecture Notes in Computer Science, pages 338-356. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_18.
  26. Igor Konnov, Marijana Lazic, Ilina Stoilkovska, and Josef Widder. Survey on parameterized verification with threshold automata and the Byzantine model checker. Logical Methods in Computer Science, 19(1), 2023. URL: https://doi.org/10.46298/LMCS-19(1:5)2023.
  27. Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), pages 719-734. Association for Computing Machinery, 2017. URL: https://doi.org/10.1145/3009837.3009860.
  28. Igor Konnov, Helmut Veith, and Josef Widder. SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms. In CAV (1), volume 9206 of Lecture Notes in Computer Science, pages 85-102. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_6.
  29. M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011), volume 6806 of LNCS, pages 585-591. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_47.
  30. Leslie Lamport. The part-time parliament. ACM Transactions on Computer Systems, 16(2):133-169, 1998. URL: https://doi.org/10.1145/279227.279229.
  31. Leslie Lamport. Fast Paxos. Distributed Computing, 19(2):79-103, 2006. URL: https://doi.org/10.1007/s00446-006-0005-x.
  32. Nancy Lynch and Frits Vaandrager. Forward and backward simulations i.: untimed systems. Information and Computation, 121(2):214-233, 1995. URL: https://doi.org/10.1006/inco.1995.1134.
  33. Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. In PODC, pages 377-410. ACM, 1990. URL: https://doi.org/10.1145/93385.93442.
  34. Tatsuya Noguchi, Tatsuhiro Tsuchiya, and Tohru Kikuno. Safety verification of asynchronous consensus algorithms with model checking. In IEEE 18th Pacific Rim International Symposium on Dependable Computing (PRDC 2012), pages 80-88. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/PRDC.2012.24.
  35. Diego Ongaro and John Ousterhout. In search of an understandable consensus algorithm. In Proceedings of the 2014 USENIX Annual Technical Conference, pages 305-320, 2014. URL: https://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro.
  36. Oded Padon, Kenneth L. McMillan, Aurojit Panda, Shmuel Sagiv, and Sharon Shoham. Ivy: safety verification by interactive generalization. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016), 2016. URL: https://api.semanticscholar.org/CorpusID:17141487.
  37. William Schultz, Edward Ashton, Heidi Howard, and Stavros Tripakis. Scalable, interpretable distributed protocol verification by inductive proof slicing. CoRR, abs/2404.18048, 2024. URL: https://doi.org/10.48550/arXiv.2404.18048.
  38. Yee Jiun Song and Robbert van Renesse. Bosco: One-Step Byzantine Asynchronous Consensus. In Gadi Taubenfeld, editor, Distributed Computing, pages 438-450, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-87779-0_30.
  39. T. K. Srikanth and Sam Toueg. Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Comput., 2(2):80-94, 1987. URL: https://doi.org/10.1007/BF01667080.
  40. Ilina Stoilkovska, Igor Konnov, Josef Widder, and Florian Zuleger. Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In Tomás Vojnar and Lijun Zhang, editors, Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Lecture Notes in Computer Science, pages 357-374. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17465-1_20.
  41. Ilina Stoilkovska, Igor Konnov, Josef Widder, and Florian Zuleger. Eliminating message counters in threshold automata. In Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA 2020), pages 196-212. Springer-Verlag, 2020. URL: https://doi.org/10.1007/978-3-030-59152-6_11.
  42. Bastien Thomas and Ocan Sankur. PyLTA: A verification tool for parameterized distributed algorithms. In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), pages 28-35. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_4.
  43. Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson. Planning for change in a formal verification of the Raft consensus protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016), pages 154-165. ACM, 2016. URL: https://doi.org/10.1145/2854065.2854081.
  44. Yang Xiao, Ning Zhang, Wenjing Lou, and Y. Thomas Hou. A survey of distributed consensus protocols for blockchain networks. IEEE Communications Surveys & Tutorials, 22(2):1432-1465, 2020. URL: https://doi.org/10.1109/COMST.2020.2969706.
  45. Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. DistAI: Data-Driven automated invariant learning for distributed protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21), pages 405-421. USENIX Association, July 2021. URL: https://www.usenix.org/conference/osdi21/presentation/yao.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact