Document Open Access Logo

Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability

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

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CP.2025.19.pdf
  • Filesize: 1.75 MB
  • 21 pages
HTML5 Logo HTML (experimental)
LIPIcs.CP.2025.19.html

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
  • Synchronous Unison
  • Satisfiability

Metrics

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

Abstract

Synchronous unison is a classical clock synchronization problem in distributed computing, and especially in self-stabilization. This paper explores the self-stabilization of a synchronous unison algorithm proposed by Arora et al. using a propositional satisfiability-based approach. We give a logical formulation of the algorithm. This formulation includes the uniqueness of clock values at each node, the updates of clocks based on the minimum clock value in the neighborhood, and the detection of convergence or divergence. To optimize the models, additional constraints are introduced to reduce redundant cases of initial configurations to be analyzed. Our approach not only verifies the algorithm’s behaviour but also offers insights into enhancing its robustness and applicability to broader distributed systems.

Cite As Get BibTex

Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert. Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CP.2025.19

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 project ANR-24-CE23-6126 (BforSAT), funded by the French National Research Agency. This work was also granted access to HPC resources of "Plateforme MatriCS" within University of Picardie Jules Verne, co-financed by the European Union with the European Regional Development Fund (FEDER) and the Hauts-De-France Regional Council among others.

Supplementary Materials

References

  1. Karine Altisen, Stéphane Devismes, and Anaïs Durand. Concurrency in snap-stabilizing local resource allocation. Journal Of Parallel and Distributed Computing, 102:42-56, 2017. URL: https://doi.org/10.1016/J.JPDC.2016.11.004.
  2. Karine Altisen, Stéphane Devismes, Anaïs Durand, Colette Johnen, and Franck Petit. Self-stabilizing systems in spite of high dynamics. Theor. Comput. Sci., 964:113966, 2023. URL: https://doi.org/10.1016/J.TCS.2023.113966.
  3. Karine Altisen, Stéphane Devismes, Swan Dubois, and Franck Petit. Introduction to Distributed Self-Stabilizing Algorithms. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool, 2019. Google Scholar
  4. Anish Arora, Shlomi Dolev, and Mohamed G. Gouda. Maintaining digital clocks in step. Parallel Processing Letters, 1:11-18, 1991. URL: https://doi.org/10.1007/bfb0022438.
  5. 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.
  6. Armin Biere. Handbook of satisfiability. In Frontiers in Artificial Intelligence and Applications, pages 75-98. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-75.
  7. 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.
  8. Armin Biere et al. Symbolic model checking without bdds. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 193-207, 1999. Google Scholar
  9. 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.
  10. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of Satisfiability: Second Edition. Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://books.google.fr/books?id=dUAvEAAAQBAJ.
  11. James E. Burns, Mohamed G. Gouda, and Raymond E. Miller. Stabilization and pseudo-stabilization. Distributed Computing, 7(1):35-42, 1993. URL: https://doi.org/10.1007/BF02278854.
  12. Fabienne Carrier, Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, and Yvan Rivierre. Self-stabilizing (f, g)-alliances with safe convergence. J. Parallel Distributed Comput., 81-82:11-23, 2015. URL: https://doi.org/10.1016/J.JPDC.2015.02.001.
  13. 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.
  14. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor, Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer, 1981. URL: https://doi.org/10.1007/BFB0025774.
  15. Stephen A. Cook. The complexity of theorem-proving procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing (STOC), pages 151-158, 1971. URL: https://doi.org/10.1145/800157.805047.
  16. J.-M. Couvreur, N. Francez, and M. G. Gouda. Asynchronous unison (extended abstract). In 12th International Conference on Distributed Computing Systems, (ICDCS'92), pages 486-493. IEEE Computer Society, 1992. URL: https://doi.org/10.1109/ICDCS.1992.235005.
  17. Stéphane Devismes, David Ilcinkas, Colette Johnen, and Frédéric Mazoit. Being efficient in time, space, and workload: a self-stabilizing unison and its consequences. In Olaf Beyersdorff, Michal Pilipczuk, Elaine Pimentel, and Kim Thang Nguyen, editors, 42nd International Symposium on Theoretical Aspects of Computer Science, STACS 2025, March 4-7, 2025, Jena, Germany, volume 327 of LIPIcs, pages 30:1-30:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPICS.STACS.2025.30.
  18. 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.
  19. 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.
  20. Danny Dolev and Dahlia Malkhi. Consensus: Perspectives and challenges. In Proceedings of the Tenth International Workshop on Distributed Algorithms (WDAG), pages 1-12, 1995. URL: https://doi.org/10.1007/3-540-60220-8_1.
  21. Shlomi Dolev and Ted Herman. Superstabilizing protocols for dynamic distributed systems. Chicago Journal of Theoretical Computer Science, 1995. Google Scholar
  22. Shlomi Dolev, Amos Israeli, and Shlomo Moran. Self-stabilization of dynamic systems assuming only read/write atomicity. Distrib. Comput., 7(1):3-16, November 1993. URL: https://doi.org/10.1007/BF02278851.
  23. Stéphane Grumbach and Zhilin Wu. Logical locality entails frugal distributed computation over graphs (extended abstract). In Christophe Paul and Michel Habib, editors, WG, volume 5911 of Lecture Notes in Computer Science, pages 154-165, 2009. URL: https://doi.org/10.1007/978-3-642-11409-0_14.
  24. Rachid Hadid. A stabilising optimal k-out-of-l resources allocation algorithm. Int. J. Knowl. Eng. Data Min., 5(3):173-194, 2018. URL: https://doi.org/10.1504/IJKEDM.2018.10014813.
  25. 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, 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.
  26. Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert. SAT_for_UNISON. Software, (visited on 2025-07-16). URL: https://github.com/asmakhoualdia98/SU_SAT_Exec
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23375
  27. Yassine Lakhnech and Michael Siegel. Deductive verification of stabilizing systems. In Sukumar Ghosh and Ted Herman, editors, 3rd Workshop on Self-stabilizing Systems, Santa Barbara, California, USA, August, 1997, Proceedings, pages 201-216. Carleton University Press, 1997. Google Scholar
  28. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 123-140. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_9.
  29. Nathan Linial. Distributive graph algorithms-global solutions from local data. In 28th Annual Symposium on Foundations of Computer Science, Los Angeles, California, USA, 27-29 October 1987, pages 331-335. IEEE Computer Society, 1987. URL: https://doi.org/10.1109/SFCS.1987.20.
  30. 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.
  31. Steven D. Prestwich. CNF encodings. 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 75-100. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200985.
  32. 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.
  33. Michael Siegel. Formal verification of stabilizing systems. In Anders P. Ravn and Hans Rischel, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, 5th International Symposium, FTRTFT'98, Lyngby, Denmark, September 14-18, 1998, Proceedings, volume 1486 of Lecture Notes in Computer Science, pages 158-172. Springer, 1998. URL: https://doi.org/10.1007/BFB0055345.
  34. Gerard Tel. Introduction to Distributed Algorithms. Cambridge University Press, 2nd edition, 2000. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact