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+\alpha)r$, where $r$ is the eccentricity of node $s$ (i.e., the maximum distance from $s$ to any other node) and $\alpha$ is any positive real constant. This task has been introduced by Duncan et al. [ACM Trans. Algorithms 2006] and is known as \emph{distance-constrained exploration}. The \emph{penalty} of an exploration algorithm running in $G$ is the number of edge traversals made by the agent in excess of $|E|$. Panaite and Pelc [J. Algorithms 1999] 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 $\mathcal{O}(|V|)$. Hence, a natural question is whether we could 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 \emph{fuel-constrained exploration}, another variant studied in the literature. This solves an open problem posed by Duncan et al. [ACM Trans. Algorithms 2006] and shows a fundamental separation with the task of exploration without constraint on the moves.

We address the perpetual grid exploration (PGE) by a swarm of autonomous, asynchronous, myopic, and luminous robots. We first show that it is impossible for the robots to explore the grid regardless of their number and the number of colors they can take if their visibility range is one. We also show that PGE is impossible with three oblivious robots that have a visibility range of two hops. We then present three optimal algorithms solving the problem. The first algorithm uses four oblivious robots with a visibility range of two, but assumes they agree on a common chirality. For the two other algorithms, no common chirality is assumed. The former uses three robots that have a visibility range of two and a two-color light. The latter uses three oblivious robots under visibility range three.

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 Theta(log(B)) bits per node and is fully polynomial as it stabilizes in at most 2D + 2 rounds and O(min(n(2)B, n(3))) 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.

In this paper, we consider the exploration of an infinite grid by a swarm of fully-synchronous robots with weak capabilities: they are disoriented, opaque, do not communicate explicitely, have limited visibility, and cannot occupy the same position at the same time. Our first result shows that, in this context, minimizing the visibility range and the number of used colors are two orthogonal issues: it is impossible to design a solution to our exploration 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. More precisely, the first algorithm solves the problem using eight oblivious robots under visibility range two (this visibility being optimal when considering oblivious robots), and the second algorithm solves the problem under visibility range one using six robots and two colors (which is optimal under this visibility range). Finally, we also tackle the optimality in terms of number of robots. According to the lower bound given in Bramas et al. (2020), we propose an algorithm working with a minimum number of robots (five) under visibility range one. This latter uses twelve colors and also guarantees that nodes are visited infinitely often. (c) 2025 The Author(s). Published by Elsevier B.V. This is an open access article under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

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.

We consider distributed systems subject to frequent topological changes. Specifically, we assume the network topology evolves as a dynamic graph in which, at any point in time, the temporal distance between any two processes is at most . Under a synchronous message-passing model where processes have unique identifiers and know both and an upper bound N on the number of processes n, we provide a distributed self-stabilizing mutual exclusion algorithm working in that class of dynamic graphs. Our solution stabilizes in 𝒪( .N) rounds using bounded local memories. Moreover, it achieves optimal waiting time: once stabilized, the maximum delay before a process enters its critical section is at most n-1 rounds. Our algorithm is actually a composition of several self-stabilizing building blocks that respectively achieve Leader Election, Unison, and Ranking. We also provide original self-stabilizing solutions for the latter two problems; for the self-stabilizing leader election, we use a solution given by Altisen et al. (Theoretical Computer Science, 2023).

Distributed systems are ubiquitous, and their distributed nature make them particularly vulnerable to faults. Being able to automatically recover from these faults is of utmost importance, and self-stabilization is a general and lightweight approach to tackle this problem. However, fully asynchronous self-stabilizing algorithms (FASS) are notoriously difficult to design and prove. It thus makes sense to create and prove a transformer that turns synchronous algorithms into FASSes. The Rollback Compiler of Awerbuch and Varghese (FOCS 1991) is such a transformer. The problem is that although it produces FASSes that are fast (time being evaluated in rounds), we prove that their energy requirement (measured through the number of state changes) can be exponential in the number n of nodes. Actually, regardless of the problem, the literature only contains a few FASSes which are asymptotically optimal time-wise. Moreover, several of these algorithms have been shown to require an exponential amount of energy, and no such algorithms are known to be energy-efficient. In this paper, we introduce the first transformer that turns any terminating synchronous algorithm into a fully asynchronous self-stabilizing algorithm with essentially the same time complexity and with a low energy requirement (polynomial in n ). However, as for the rollback compiler, this comes at the cost of a (reasonable) memory increase. Our approach is compatible with most models, ranging from the LOCAL model (a powerful synchronous fault-free model), down to models such as the Stone Age model, in which a node cannot even know how many neighbors it has. In particular, we can transform extremely fast algorithms such as the classical Θ{ log*n )-time ring coloring algorithm by Cole and Vishkin (FOCS 1986) into fast and energy-efficient FASSes. We also provide the best FASSes so far for many classical distributed problems such as leader election and spanning tree constructions ( e.g. , BFS, shortest-path).

We consider identified directed networks where processes know an upper bound on the maximum ancestor distance. Under these settings, we study the conditions on the network topology allowing the self-stabilization of two fundamental problems: the leader election and the synchronous unison. We show that those two problems can be self-stabilizingly solved in our settings if and only if the network contains a unique source component. In particular, to show that our condition is sufficient, we propose two algorithms and study their complexity. Notice that our topological condition covers a wide spectrum of digraphs since, for example, strongly connected digraphs, dipaths, and out-trees have a unique source component.

Self-stabilization is a general paradigm that characterizes the ability of a distributed system to recover from transient faults. Since its introduction by Dijkstra in 1974, self-stabilization has been successfully applied to efficiently solve many networking tasks. However, most of the literature focuses on bidirectional networks. Now, in today’s networks such as WSNs, some communication channels may be one-way only. Considering such network topologies, a.k.a. directed graphs, makes self-stabilization more complicated, and sometimes even impossible. In this paper, we investigate the gap in terms of requirements and efficiency when considering a directed graph instead of an undirected one as network topology for a self-stabilizing algorithm. Our case study is a variant of a synchronous unison algorithm proposed by Arora et al.; the synchronous unison being a clock synchronization problem.

We address the perpetual grid exploration by a swarm of autonomous, asynchronous, myopic, and luminous robots. We first show that it is impossible for the robots to explore the grid regardless of their number and the number of colors they can take if their visibility range is one. We also show that PGE is impossible with three oblivious robots that have a visibility range of two hops. We then present three optimal algorithms solving the problem. The first algorithm uses four oblivious robots with a visibility range of two, but assumes they agree on a common chirality. For the two other algorithms, no common chirality is assumed. The former uses three robots that have a visibility range of two and a two-color light. The latter uses three oblivious robots under visibility range three.

This paper deals with the trade-off between time, workload, and versatility in self-stabilization, a general and lightweight fault-tolerant concept in distributed computing.In this context, we propose a transformer that provides an asynchronous silent self-stabilizing version Trans(AlgI) of any terminating synchronous algorithm AlgI. The transformed algorithm Trans(AlgI) works under the distributed unfair daemon and is efficient both in moves and rounds.Our transformer allows to easily obtain fully-polynomial silent self-stabilizing solutions that are also asymptotically optimal in rounds.We illustrate the efficiency and versatility of our transformer with several efficient (i.e., fully-polynomial) silent self-stabilizing instances solving major distributed computing problems, namely vertex coloring, Breadth-First Search (BFS) spanning tree construction, k-clustering, and leader election.

We present a self-stabilizing algorithm for the (asynchronous) unison problem which achieves an efficient trade-off between time, workload, and space in a weak model. Precisely, our algorithm is defined in the atomic-state model and works in anonymous 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 a $n$-node network of diameter $D$ and assuming a period $B \geq 2D+2$, our algorithm only requires $O(\log B)$ bits per node to achieve full polynomiality as it stabilizes in at most $2D-2$ rounds and $O(\min(n^2B, n^3))$ moves. In particular and to the best of our knowledge, it is the first self-stabilizing unison for arbitrary anonymous networks achieving an asymptotically optimal stabilization time in rounds using a bounded memory at each node. Finally, we show that our solution allows to efficiently simulate synchronous self-stabilizing algorithms in an asynchronous environment. This provides a new state-of-the-art algorithm solving both the leader election and the spanning tree construction problem in any identified connected network which, to the best of our knowledge, beat all existing solutions of the literature.

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.