Document Open Access Logo

Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms

Authors Nathalie Bertrand , Bastien Thomas, Josef Widder

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2021.15.pdf
  • Filesize: 0.77 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • Theory of computation → Distributed algorithms
Keywords
  • Verification
  • Distributed algorithms
  • Domain theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Distributed algorithms typically run over arbitrary many processes and may involve unboundedly many rounds, making the automated verification of their correctness challenging. Building on domain theory, we introduce a framework that abstracts infinite-state distributed systems that represent distributed algorithms into finite-state guard automata. The soundness of the approach corresponds to the Scott-continuity of the abstraction, which relies on the assumption that the distributed algorithms are layered. Guard automata thus enable the verification of safety and liveness properties of distributed algorithms.

Cite As Get BibTex

Nathalie Bertrand, Bastien Thomas, and Josef Widder. Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CONCUR.2021.15

Author Details

Nathalie Bertrand
  • Université Rennes, Inria, CNRS, IRISA, France
Bastien Thomas
  • Université Rennes, Inria, CNRS, IRISA, France
Josef Widder
  • Informal Systems, Wien, Austria

Funding

This project has received funding from Interchain Foundation (Switzerland).

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Zeinab Ganjei, Ahmed Rezine, and Yunyun Zhu. Verification of cache coherence protocols wrt. trace filters. In Proceedings of the 15th International Conference on Formal Methods in Computer-Aided Design (FMCAD'15), pages 9-16. IEEE, 2015. Google Scholar
  2. Samson Abramsky and Achim Jung. Domain Theory, volume 3 of Handbook of Logic in Computer Science, pages 1-168. Clarendon Press, 1994. Google Scholar
  3. C. Aiswarya, Benedikt Bollig, and Paul Gastin. An automata-theoretic approach to the verification of distributed algorithms. Information and Computation, 259:305-327, 2018. Google Scholar
  4. Francesco Alberti, Silvio Ghilardi, and Elena Pagani. Counting constraints in flat array fragments. In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR'16), volume 9706 of Lecture Notes in Computer Science, pages 65-81, 2016. Google Scholar
  5. A. R. Balasubramanian, Javier Esparza, and Marijana Lazić. Complexity of verification and synthesis of threshold automata. In Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20), volume 12302 of Lecture Notes in Computer Science, pages 144-160. Springer, 2020. Google Scholar
  6. Michael Ben-Or. Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract). In Proceedings of the 2nd Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC'83), pages 27-30, 1983. Google Scholar
  7. Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, and Sharon Shoham. Verification of threshold-based distributed algorithms by decomposition to decidable logics. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV'19), volume 11562 of Lecture Notes in Computer Science, pages 245-266. Springer, 2019. Google Scholar
  8. Piotr Berman and Juan A. Garay. Cloture votes: n/4-resilient distributed consensus in t+1 rounds. Mathematical Systems Theory, 26(1):3-19, 1993. Google Scholar
  9. 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. Google Scholar
  10. Luca Bortolussi and Jane Hillston. Model checking single agent behaviours by fluid approximation. Information and Computation, 242:183-226, 2015. Google Scholar
  11. Gabriel Bracha and Sam Toueg. Asynchronous consensus and broadcast protocols. Journal of the ACM, 32(4):824-840, 1985. Google Scholar
  12. 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'09), volume 5797 of Lecture Notes in Computer Science, pages 93-106, 2009. Google Scholar
  13. Bernadette Charron-Bost and André Schiper. The heard-of model: computing in distributed systems with benign faults. Distributed Computing, 22(1):49-71, 2009. Google Scholar
  14. Andrei Damian, Cezara Drăgoi, Alexandru Militaru, and Josef Widder. Communication-closed asynchronous protocols. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV'19), volume 11562 of Lecture Notes in Computer Science, pages 344-363. Springer, 2019. Google Scholar
  15. Nicolaas G. de Bruijn. A combinatorial problem. Indagationes Mathematicae, 49:758-764, 1946. Google Scholar
  16. Cezara Drăgoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. A Logic-Based Framework for Verifying Consensus Algorithms. In Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'14), volume 8318 of Lecture Notes in Computer Science, pages 161-181, 2014. Google Scholar
  17. Tzilla Elrad and Nissim Francez. Decomposition of distributed programs into communication-closed layers. Science of Computer Programming, 2(3):155-173, 1982. Google Scholar
  18. Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science (STACS'14), volume 25 of LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. Google Scholar
  19. 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'17), pages 719-734, 2017. Google Scholar
  20. Igor Konnov, Helmut Veith, and Josef Widder. On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation, 252:95-109, 2017. Google Scholar
  21. Jure Kukovec, Igor Konnov, and Josef Widder. Reachability in parameterized systems: All flavors of threshold automata. In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR'18), volume 118 of LIPIcs, pages 19:1-19:17, 2018. Google Scholar
  22. Leslie Lamport. Checking a multithreaded algorithm with ^+CAL. In Proceedings of the 20th International Symposium on Distributed Computing (DISC'06), volume 4167 of Lecture Notes in Computer Science, pages 151-163. Springer, 2006. Google Scholar
  23. Richard J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717-721, 1975. Google Scholar
  24. Ognjen Maric, Christoph Sprenger, and David A. Basin. Cutoff bounds for consensus algorithms. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV'17), volume 10427 of Lecture Notes in Computer Science, pages 217-237, 2017. Google Scholar
  25. Kenneth L. McMillan. Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01), volume 2144, pages 179-195. Springer, 2001. Google Scholar
  26. Dominique Méry. Verification by Construction of Distributed Algorithms. In Proceedings of the 16th International Colloquium on Theoretical Aspects of Computing (ICTAC'19), volume 11884 of Lecture Notes in Computer Science, pages 22-38. Springer, 2019. Google Scholar
  27. Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru, and Sébastien Tixeuil. Parameterized verification of algorithms for oblivious robots on a ring. In Proceedings of the 17th International Conference on Formal Methods in Computer Aided Design (FMCAD'17), pages 212-219. IEEE, 2017. Google Scholar
  28. Ocan Sankur and Jean-Pierre Talpin. An abstraction technique for parameterized model checking of leader election protocols: Application to FTSP. In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), volume 10205 of Lecture Notes in Computer Science, pages 23-40, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_2.
  29. Ilina Stoilkovska, Igor Konnov, Josef Widder, and Florian Zuleger. Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), volume 11428 of Lecture Notes in Computer Science, pages 357-374, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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