Search Results

Documents authored by Devismes, Stéphane

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}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.68
Graph Exploration: The Impact of a Distance Constraint

Authors: Stéphane Devismes, Yoann Dieudonné, and Arnaud Labourel

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
A mobile agent, starting from a node s of a simple undirected connected graph G = (V,E), has to explore all nodes and edges of G using the minimum number of edge traversals. To do so, the agent uses a deterministic algorithm that allows it to gain information on G as it traverses its edges. During its exploration, the agent must always respect the constraint of knowing a path of length at most D to go back to node s. The upper bound D is fixed as being equal to (1+α)r, where r is the eccentricity of node s (i.e., the maximum distance from s to any other node) and α is any positive real constant. This task has been introduced by Duncan et al. [Christian A. Duncan et al., 2006] and is known as distance-constrained exploration. The penalty of an exploration algorithm running in G is the number of edge traversals made by the agent in excess of |E|. In [Petrisor Panaite and Andrzej Pelc, 1999], Panaite and Pelc gave an algorithm for solving exploration without any constraint on the moves that is guaranteed to work in every graph G with a (small) penalty in 𝒪(|V|). Hence, a natural question is whether we can obtain a distance-constrained exploration algorithm with the same guarantee as well. In this paper, we provide a negative answer to this question. We also observe that an algorithm working in every graph G with a linear penalty in |V| cannot be obtained for the task of fuel-constrained exploration, another variant studied in the literature. This solves an open problem posed by Duncan et al. in [Christian A. Duncan et al., 2006] and shows a fundamental separation with the task of exploration without constraint on the moves.
Cite as

Stéphane Devismes, Yoann Dieudonné, and Arnaud Labourel. Graph Exploration: The Impact of a Distance Constraint. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 68:1-68:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{devismes_et_al:LIPIcs.ICALP.2025.68,
  author =	{Devismes, St\'{e}phane and Dieudonn\'{e}, Yoann and Labourel, Arnaud},
  title =	{{Graph Exploration: The Impact of a Distance Constraint}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{68:1--68:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.68},
  URN =		{urn:nbn:de:0030-drops-234452},
  doi =		{10.4230/LIPIcs.ICALP.2025.68},
  annote =	{Keywords: exploration, graph, mobile agent}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.30
Being Efficient in Time, Space, and Workload: a Self-Stabilizing Unison and Its Consequences

Authors: Stéphane Devismes, David Ilcinkas, Colette Johnen, and Frédéric Mazoit

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
We present a self-stabilizing algorithm for the unison problem which is efficient in time, workload, and space in a weak model. Precisely, our algorithm is defined in the atomic-state model and works in anonymous asynchronous connected networks in which even local ports are unlabeled. It makes no assumption on the daemon and thus stabilizes under the weakest one: the distributed unfair daemon. In an n-node network of diameter D and assuming the knowledge B ≥ 2D+2, our algorithm only requires Θ(log(B)) bits per node and is fully polynomial as it stabilizes in at most 2D+2 rounds and O(min(n²B, n³)) moves. In particular, it is the first self-stabilizing unison for arbitrary asynchronous anonymous networks achieving an asymptotically optimal stabilization time in rounds using a bounded memory at each node. Furthermore, we show that our solution can be used to efficiently simulate synchronous self-stabilizing algorithms in asynchronous environments. For example, this simulation allows us to design a new state-of-the-art algorithm solving both the leader election and the BFS (Breadth-First Search) spanning tree construction in any identified connected network which, to the best of our knowledge, beats all existing solutions in the literature.
Cite as

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 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{devismes_et_al:LIPIcs.STACS.2025.30,
  author =	{Devismes, St\'{e}phane and Ilcinkas, David and Johnen, Colette and Mazoit, Fr\'{e}d\'{e}ric},
  title =	{{Being Efficient in Time, Space, and Workload: a Self-Stabilizing Unison and Its Consequences}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.30},
  URN =		{urn:nbn:de:0030-drops-228568},
  doi =		{10.4230/LIPIcs.STACS.2025.30},
  annote =	{Keywords: Self-stabilization, unison, time complexity, synchronizer}
}
Document
DOI: 10.4230/LIPIcs.DISC.2023.2
Certified Round Complexity of Self-Stabilizing Algorithms

Authors: Karine Altisen, Pierre Corbineau, and Stéphane Devismes

Published in: LIPIcs, Volume 281, 37th International Symposium on Distributed Computing (DISC 2023)

Abstract
A proof assistant is an appropriate tool to write sound proofs. The need of such tools in distributed computing grows over the years due to the scientific progress that leads algorithmic designers to consider always more difficult problems. In that spirit, the PADEC Coq library has been developed to certify self-stabilizing algorithms. Efficiency of self-stabilizing algorithms is mainly evaluated by comparing their stabilization times in rounds, the time unit that is primarily used in the self-stabilizing area. In this paper, we introduce the notion of rounds in the PADEC library together with several formal tools to help the certification of the complexity analysis of self-stabilizing algorithms. We validate our approach by certifying the stabilization time in rounds of the classical Dolev et al’s self-stabilizing Breadth-first Search spanning tree construction.
Cite as

Karine Altisen, Pierre Corbineau, and Stéphane Devismes. Certified Round Complexity of Self-Stabilizing Algorithms. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 2:1-2:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{altisen_et_al:LIPIcs.DISC.2023.2,
  author =	{Altisen, Karine and Corbineau, Pierre and Devismes, St\'{e}phane},
  title =	{{Certified Round Complexity of Self-Stabilizing Algorithms}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{2:1--2:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2023.2},
  URN =		{urn:nbn:de:0030-drops-191284},
  doi =		{10.4230/LIPIcs.DISC.2023.2},
  annote =	{Keywords: Certification, proof assistant, Coq, self-stabilization, round complexity}
}
Document
DOI: 10.4230/LIPIcs.FUN.2022.7
Beedroids: How Luminous Autonomous Swarms of UAVs Can Save the World?

Authors: Quentin Bramas, Stéphane Devismes, Anaïs Durand, Pascal Lafourcade, and Anissa Lamani

Published in: LIPIcs, Volume 226, 11th International Conference on Fun with Algorithms (FUN 2022)

Abstract
Bee extinction is a great risk for humanity. To circumvent this ineluctable disaster, we propose to develop beedroids, i.e., small UAVs mimicking the behaviors of real bees. Those beedroids are endowed with very weak capabilities (short-range visibility sensors, no GPS, light with a few colors, ...). Like real bees, they have to self-organize together into swarms. Beedroid swarms will be deployed in cuboid-shaped greenhouse. Each beedroid swarm will have to indefinitely search for flowers to pollinate in its greenhouse. We model this problem as a perpetual exploration of a 3D grid by a swarm of beedroids. In this paper, we propose two optimal solutions to solve this problem and so to save humanity.
Cite as

Quentin Bramas, Stéphane Devismes, Anaïs Durand, Pascal Lafourcade, and Anissa Lamani. Beedroids: How Luminous Autonomous Swarms of UAVs Can Save the World?. In 11th International Conference on Fun with Algorithms (FUN 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 226, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bramas_et_al:LIPIcs.FUN.2022.7,
  author =	{Bramas, Quentin and Devismes, St\'{e}phane and Durand, Ana\"{i}s and Lafourcade, Pascal and Lamani, Anissa},
  title =	{{Beedroids: How Luminous Autonomous Swarms of UAVs Can Save the World?}},
  booktitle =	{11th International Conference on Fun with Algorithms (FUN 2022)},
  pages =	{7:1--7:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-232-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{226},
  editor =	{Fraigniaud, Pierre and Uno, Yushi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2022.7},
  URN =		{urn:nbn:de:0030-drops-159771},
  doi =		{10.4230/LIPIcs.FUN.2022.7},
  annote =	{Keywords: Bee extinction, luminous swarms of beedroids, perpetual flower pollination problem, greenhouse}
}
Document
DOI: 10.4230/LIPIcs.FUN.2021.6
Finding Water on Poleless Using Melomaniac Myopic Chameleon Robots

Authors: Quentin Bramas, Pascal Lafourcade, and Stéphane Devismes

Published in: LIPIcs, Volume 157, 10th International Conference on Fun with Algorithms (FUN 2021) (2020)

Abstract
In 2042, the exoplanet exploration program, launched in 2014 by NASA, finally discovers a new exoplanet so-called Poleless, due to the fact that it is not subject to any magnetism. A new generation of autonomous mobile robots, called M2C (for Melomaniac Myopic Chameleon), have been designed to find water on Poleless. To address this problem, we investigate optimal (w.r.t., visibility range and number of used colors) solutions to the infinite grid exploration problem (IGE) by a small team of M2C robots. Our first result shows that minimizing the visibility range and the number of used colors are two orthogonal issues: it is impossible to design a solution to the IGE problem that is optimal w.r.t. both parameters simultaneously. Consequently, we address optimality of these two criteria separately by proposing two algorithms; the former being optimal in terms of visibility range, the latter being optimal in terms of number of used colors. It is worth noticing that these two algorithms use a very small number of robots, respectively six and eight.
Cite as

Quentin Bramas, Pascal Lafourcade, and Stéphane Devismes. Finding Water on Poleless Using Melomaniac Myopic Chameleon Robots. In 10th International Conference on Fun with Algorithms (FUN 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 157, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bramas_et_al:LIPIcs.FUN.2021.6,
  author =	{Bramas, Quentin and Lafourcade, Pascal and Devismes, St\'{e}phane},
  title =	{{Finding Water on Poleless Using Melomaniac Myopic Chameleon Robots}},
  booktitle =	{10th International Conference on Fun with Algorithms (FUN 2021)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-145-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{157},
  editor =	{Farach-Colton, Martin and Prencipe, Giuseppe and Uehara, Ryuhei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2021.6},
  URN =		{urn:nbn:de:0030-drops-127674},
  doi =		{10.4230/LIPIcs.FUN.2021.6},
  annote =	{Keywords: Luminous Robots, Grid, Infinite Exploration, Treasure Search Problem}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2016.10
Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps

Authors: Stéphane Devismes, David Ilcinkas, and Colette Johnen

Published in: LIPIcs, Volume 70, 20th International Conference on Principles of Distributed Systems (OPODIS 2016)

Abstract
We deal with the problem of maintaining a shortest-path tree rooted at some process r in a network that may be disconnected after topological changes. The goal is then to maintain a shortest-path tree rooted at r in its connected component, V_r, and make all processes of other components detecting that r is not part of their connected component. We propose, in the composite atomicity model, a silent self-stabilizing algorithm for this problem working in semi-anonymous networks under the distributed unfair daemon (the most general daemon) without requiring any a priori knowledge about global parameters of the network. This is the first algorithm for this problem that is proven to achieve a polynomial stabilization time in steps. Namely, we exhibit a bound in O(W_{max} * n_{maxCC}^3 * n), where W_{max} is the maximum weight of an edge, n_{maxCC} is the maximum number of non-root processes in a connected component, and n is the number of processes. The stabilization time in rounds is at most 3n_{maxCC} + D, where D is the hop-diameter of V_r.
Cite as

Stéphane Devismes, David Ilcinkas, and Colette Johnen. Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{devismes_et_al:LIPIcs.OPODIS.2016.10,
  author =	{Devismes, St\'{e}phane and Ilcinkas, David and Johnen, Colette},
  title =	{{Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps}},
  booktitle =	{20th International Conference on Principles of Distributed Systems (OPODIS 2016)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-031-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{70},
  editor =	{Fatourou, Panagiota and Jim\'{e}nez, Ernesto and Pedone, Fernando},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2016.10},
  URN =		{urn:nbn:de:0030-drops-70792},
  doi =		{10.4230/LIPIcs.OPODIS.2016.10},
  annote =	{Keywords: distributed algorithm, self-stabilization, routing algorithm, shortest path, disconnected network, shortest-path tree}
}
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