Search Results

Documents authored by Khoualdia, Asma

Artifact
Software
DOI: 10.4230/artifacts.26907
SAT_for_TOKEN

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

Abstract
Cite as

Asma Khoualdia, Sami Cherif, Stéphane Devismes, Léo Robert. SAT_for_TOKEN (Software, Source Code and Benchmarks). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26907,
   title = {{SAT\underlinefor\underlineTOKEN}}, 
   author = {Khoualdia, Asma and Cherif, Sami and Devismes, St\'{e}phane and Robert, L\'{e}o},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:0fe597aebfaba66c4b306d44a44a9e49dcf277d5;origin=https://github.com/asmakhoualdia98/async-token-circulation-sat;visit=swh:1:snp:ae3075e2950c87577ec2f3dabe7f025019446011;anchor=swh:1:rev:de00109298c91e2a931f90806309c549b1e4e247}{\texttt{swh:1:dir:0fe597aebfaba66c4b306d44a44a9e49dcf277d5}} (visited on 2026-07-13)},
   url = {https://github.com/asmakhoualdia98/async-token-circulation-sat},
   doi = {10.4230/artifacts.26907},
}
Document
DOI: 10.4230/LIPIcs.CP.2026.32
On the Self-Stabilization of Dijkstra’s Asynchronous Token Circulation

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

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{khoualdia_et_al:LIPIcs.CP.2026.32,
  author =	{Khoualdia, Asma and Cherif, Sami and Devismes, St\'{e}phane and Robert, L\'{e}o},
  title =	{{On the Self-Stabilization of Dijkstra’s Asynchronous Token Circulation}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.32},
  URN =		{urn:nbn:de:0030-drops-266645},
  doi =		{10.4230/LIPIcs.CP.2026.32},
  annote =	{Keywords: Self-stabilization, Token Circulation, Asynchronism, Satisfiability}
}
Artifact
Software
DOI: 10.4230/artifacts.23375
SAT_for_UNISON

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

Abstract
Cite as

Asma Khoualdia, Sami Cherif, Stéphane Devismes, Léo Robert. SAT_for_UNISON (Software, Source Code and Benchmarks). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23375,
   title = {{SAT\underlinefor\underlineUNISON}}, 
   author = {Khoualdia, Asma and Cherif, Sami and Devismes, St\'{e}phane and Robert, L\'{e}o},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:4bc78d189155024f85110cb2dc9ae4aeb470d8bf;origin=https://github.com/asmakhoualdia98/SU_SAT_Exec;visit=swh:1:snp:af5a3ce14a7b5fdca4086ba55a5d21370fe4d3cb;anchor=swh:1:rev:6905da4a2f2dd404ea072c647393ba1f58ba0b4c}{\texttt{swh:1:dir:4bc78d189155024f85110cb2dc9ae4aeb470d8bf}} (visited on 2025-08-08)},
   url = {https://github.com/asmakhoualdia98/SU_SAT_Exec},
   doi = {10.4230/artifacts.23375},
}
Document
DOI: 10.4230/LIPIcs.CP.2025.19
Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability

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

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{khoualdia_et_al:LIPIcs.CP.2025.19,
  author =	{Khoualdia, Asma and Cherif, Sami and Devismes, St\'{e}phane and Robert, L\'{e}o},
  title =	{{Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{19:1--19:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.19},
  URN =		{urn:nbn:de:0030-drops-238806},
  doi =		{10.4230/LIPIcs.CP.2025.19},
  annote =	{Keywords: Self-stabilization, Synchronous Unison, Satisfiability}
}
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