Document Open Access Logo

On the Self-Stabilization of Dijkstra’s Asynchronous Token Circulation

Authors Asma Khoualdia , Sami Cherif , Stéphane Devismes , Léo Robert

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.32.pdf
  • Filesize: 2.82 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed algorithms
  • Theory of computation → Constraint and logic programming
  • Theory of computation → Logic and verification
Keywords
  • Self-stabilization
  • Token Circulation
  • Asynchronism
  • Satisfiability

Metrics

Abstract

Dijkstra’s token ring algorithm is a fundamental example of a self-stabilizing algorithm for solving mutual exclusion in an asynchronous distributed system arranged as a rooted directed ring. This paper studies the self-stabilization of this algorithm using an approach based on propositional satisfiability. We propose a logical modeling framework for the asynchronous executions of the algorithm that rigorously captures the state update rules, as well as the mechanisms for detecting convergence toward a legitimate configuration or, conversely, divergence through the existence of cycles between illegitimate configurations. Furthermore, we also optimize the efficiency and scalability of the analysis by introducing an offset-based symmetry-breaking technique applied to the initial configurations, thereby significantly reducing redundant explorations of equivalent execution scenarios. In addition, we extend the study to restricted daemon assumptions to assess open challenges.

Cite As Get BibTex

Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert. On the Self-Stabilization of Dijkstra’s Asynchronous Token Circulation. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.32

Author Details

Asma Khoualdia
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Sami Cherif
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Stéphane Devismes
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Léo Robert
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France

Funding

This work is supported by the projects ANR-22-EXES-0009 (PIA4 MAIA, France 2030) and ANR-24-CE23-6126 (BforSAT), funded by the French National Research Agency. It was also granted access to HPC resources of "Plateforme MatriCS" within University of Picardie Jules Verne, co-funded by the European Union with the European Regional Development Fund (FEDER) and the Hauts-de-France Regional Council.

Supplementary Materials

References

  1. Karine Altisen, Pierre Corbineau, and Stéphane Devismes. Certification of an exact worst-case self-stabilization time. Theor. Comput. Sci., 941:262-277, 2023. URL: https://doi.org/10.1016/J.TCS.2022.11.019.
  2. Karine Altisen, Stéphane Devismes, Swan Dubois, and Franck Petit. Introduction to Distributed Self-Stabilizing Algorithms. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2019. URL: https://doi.org/10.2200/S00908ED1V01Y201903DCT015.
  3. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks and their applications. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 167-180. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_18.
  4. Armin Biere. Bounded model checking. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 739-764. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201002.
  5. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. Cadical 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  6. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  7. Dominique Cansell, Dominique Méry, and Stephan Merz. Formal analysis of a self-stabilizing algorithm using predicate diagrams. In Kurt Bauknecht, Wilfried Brauer, and Thomas A. Mück, editors, Tagungsband der GI/OCG-Jahrestagung - 31. Jahrestagung der Gesellschaft für Informatik, Wirtschaft und Wissenschaft in der Network Economy - Visionen und Wirklichkeit, Jahrestagung der Österreichischen Computer Gesellschaft 2001, INFORMATIK/OCG 2001, Vienna, Austria, September 25-28, 2001, Band 1, volume 157 of Schriftenreihe der Österreichischen Computer-Gesellschaft, pages 628-634. Konstanz UVK-Verl.-Ges., 2001. Google Scholar
  8. Jingshu Chen and Sandeep S. Kulkarni. Smt-based model checking for stabilizing programs^,. In Davide Frey, Michel Raynal, Saswati Sarkar, Rudrapatna K. Shyamasundar, and Prasun Sinha, editors, Distributed Computing and Networking, 14th International Conference, ICDCN 2013, Mumbai, India, January 3-6, 2013. Proceedings, volume 7730 of Lecture Notes in Computer Science, pages 393-407. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-35668-1_27.
  9. Zeev Collin and Shlomi Dolev. Self-stabilizing depth-first search. Inf. Process. Lett., 49(6):297-301, 1994. URL: https://doi.org/10.1016/0020-0190(94)90103-1.
  10. Stephen A. Cook. The complexity of theorem-proving procedures. In Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman, editors, Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151-158. ACM, 1971. URL: https://doi.org/10.1145/800157.805047.
  11. Alain Cournier, Ajoy Kumar Datta, Stéphane Devismes, Franck Petit, and Vincent Villain. The expressive power of snap-stabilization. Theor. Comput. Sci., 626:40-66, 2016. URL: https://doi.org/10.1016/J.TCS.2016.01.036.
  12. Jean-Michel Couvreur, Nissim Francez, and Mohamed G. Gouda. Asynchronous unison (extended abstract). In The 12th International Conference on Distributed Computing Systems (ICDCS), pages 486-493. IEEE Computer Society, 1992. URL: https://doi.org/10.1109/ICDCS.1992.235005.
  13. Ajoy K. Datta and Lawrence L. Larmore. Self-stabilizing leader election in dynamic networks. Theory Comput. Syst., 62(5):977-1047, 2018. URL: https://doi.org/10.1007/S00224-017-9758-9.
  14. Edsger W. Dijkstra. Self-stabilizing systems in spite of distributed control. Commun. ACM, 17(11):643-644, 1974. URL: https://doi.org/10.1145/361179.361202.
  15. Danny Dolev, Keijo Heljanko, Matti Järvisalo, Janne H. Korhonen, Christoph Lenzen, Joel Rybicki, Jukka Suomela, and Siert Wieringa. Synchronous counting and computational algorithm design. J. Comput. Syst. Sci., 82(2):310-332, 2016. URL: https://doi.org/10.1016/J.JCSS.2015.09.002.
  16. Fathiyeh Faghih, Borzoo Bonakdarpour, Sébastien Tixeuil, and Sandeep S. Kulkarni. Automated synthesis of distributed self-stabilizing protocols. Log. Methods Comput. Sci., 14(1), 2018. URL: https://doi.org/10.23638/LMCS-14(1:12)2018.
  17. Wan J. Fokkink, Jaap-Henk Hoepman, and Jun Pang. A note on k-state self-stabilization in a ring with k=n. Nord. J. Comput., 12(1):18-26, 2005. Google Scholar
  18. Alexey Ignatiev, António Morgado, and João Marques-Silva. Pysat: A python toolkit for prototyping with SAT oracles. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 428-437. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
  19. Erwan Jahier, Karine Altisen, Stéphane Devismes, and Gabriel B. Sant'Anna. Model checking of distributed algorithms using synchronous programs. Theor. Comput. Sci., 1045:115292, 2025. URL: https://doi.org/10.1016/J.TCS.2025.115292.
  20. Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert. SAT_for_TOKEN. Software, (visited on 2026-06-26). URL: https://github.com/asmakhoualdia98/async-token-circulation-sat
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26907
  21. Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert. Analyzing self-stabilization of synchronous unison via propositional satisfiability. In Maria Garcia de la Banda, editor, 31st International Conference on Principles and Practice of Constraint Programming, CP 2025, Glasgow, Scotland, August 10-15, 2025, volume 340 of LIPIcs, pages 19:1-19:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CP.2025.19.
  22. Masahiro Kimoto, Tatsuhiro Tsuchiya, and Tohru Kikuno. On the time complexity of dijkstra’s three-state mutual exclusion algorithm. IEICE Trans. Inf. Syst., 92-D(8):1570-1573, 2009. URL: https://doi.org/10.1587/TRANSINF.E92.D.1570.
  23. Sandeep S. Kulkarni, John M. Rushby, and Natarajan Shankar. A case-study in component-based mechanical verification of fault-tolerant programs. In Anish Arora, editor, 1999 ICDCS Workshop on Self-stabilizing Systems, Austin, Texas, USA, June 5, 1999, Proceedings, pages 33-40. IEEE Computer Society, 1999. Google Scholar
  24. João P. Marques-Silva and Karem A. Sakallah. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  25. Stephan Merz. On the verification of a self-stabilizing algorithm. Technical report, University of Munich, 1998. Google Scholar
  26. Shaz Qadeer and Natarajan Shankar. Verifying a self-stabilizing mutual exclusion algorithm. In David Gries and Willem P. de Roever, editors, Programming Concepts and Methods, IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET '98) 8-12 June 1998, Shelter Island, New York, USA, volume 125 of IFIP Conference Proceedings, pages 424-443. Chapman & Hall, 1998. Google Scholar
  27. Olivier Roussel and Vasco Manquinho. Pseudo-boolean and cardinality constraints. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1087-1129. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201012.
  28. Tatsuhiro Tsuchiya, Shin'ichi Nagano, Rohayu Bt Paidi, and Tohru Kikuno. Symbolic model checking for self-stabilizing algorithms. IEEE Trans. Parallel Distributed Syst., 12(1):81-95, 2001. URL: https://doi.org/10.1109/71.899941.
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