Search

In this paper, we revisit the problem of classical \textit{meeting times} of random walks in graphs. In the process that two tokens (called agents) perform random walks on an undirected graph, the meeting times are defined as the expected times until they meet when the two agents are initially located at different vertices. A key feature of the problem is that, in each discrete time-clock (called \textit{round}) of the process, the scheduler selects only one of the two agents, and the agent performs one move of the random walk. In the adversarial setting, the scheduler utilizes the strategy that intends to \textit{maximizing} the expected time to meet. In the seminal papers \cite{collisions,israeli1990token,tetali1993simult}, for the random walks of two agents, the notion of \textit{atomicity} is implicitly considered. That is, each move of agents should complete while the other agent waits. In this paper, we consider and formalize the meeting time of \textit{non-atomic} random walks. In the non-atomic random walks, we assume that in each round, only one agent can move but the move does not necessarily complete in the next round. In other words, we assume that an agent can move at a round while the other agent is still moving on an edge. For the non-atomic random walks with the adversarial schedulers, we give a polynomial upper bound on the meeting times., 18 pages, 1 figure

We consider a variant of the crash-fault gathering problem called stand-up indulgent gathering (SUIG). In this problem, a group of mobile robots must eventually gather at a single location, which is not known in advance. If no robots crash, they must all meet at the same location. However, if one or more robots crash at a single location, all non-crashed robots must eventually gather at that location. The SUIG problem was first introduced for robots operating in a two-dimensional continuous Euclidean space, with most solutions relying on the ability of robots to move a prescribed (real) distance at each time instant. In this paper, we investigate the SUIG problem for robots operating in a discrete universe (i.e., a graph) where they can only move one unit of distance (i.e., to an adjacent node) at each time instant. Specifically, we focus on line-shaped networks and characterize the solvability of the SUIG problem for oblivious robots without multiplicity detection.

It is almost fifty years since Dijkstra coined the term "self-stabilization" to denote a distributed system able to recover correct behavior starting from any arbitrary (even unreachable) configuration. His seminal paper triggered many works since then, exploring over the years new variants of the original concept, new application domains, and new complexity results. While the huge majority of those contributions relates to theory, considering computability and worst case complexity issues, this talk revisits old and recent contributions from the prism of "realistic" distributed systems, aiming to address the following question: is self-stabilization relevant in practice for distributed systems?, LIPIcs, Vol. 253, 26th International Conference on Principles of Distributed Systems (OPODIS 2022), pages 3:1-3:1

International audience; It is almost fifty years since Dijkstra coined the term "self-stabilization" to denote a distributed system able to recover correct behavior starting from any arbitrary (even unreachable) configuration. His seminal paper triggered many works since then, exploring over the years new variants of the original concept, new application domains, and new complexity results. While the huge majority of those contributions relates to theory, considering computability and worst case complexity issues, this talk revisits old and recent contributions from the prism of ``realistic'' distributed systems, aiming to address the following question: is self-stabilization relevant in practice for distributed systems?

In this paper, we consider the problem of semi-uniform deployment for mobile robots in perfect ℓ-ary trees, where every intermediate node has ℓ children, and all leaf nodes have the same depth. This problem requires robots to spread in the tree so that, for some positive integer d and some fixed integer s(0≤s≤d−1), each node of depth s+dj (j≥0) is occupied by a robot. In other words, after semi-uniform deployment is achieved, nodes of depth s,s+d,s+2d,… are occupied by a robot. Robots have an infinite visibility range but are opaque, that is, robot ri cannot observe some robot rj if there exists another robot rk in the path between ri and rj. In addition, each robot can emit a light color visible to itself and other robots, taken from a set of κ colors, at each time step. Then, we clarify the relationship between the number of available light colors and the solvability of the semi-uniform deployment problem. First, we consider robots with the minimum number of available light colors, that is, robots with κ=1 (in this case, robots are oblivious). In this setting, we show that there is no collision-free algorithm to solve the semi-uniform deployment problem with explicit termination. Next, we relax the number of available light colors, that is, we consider robots with κ=2. In this setting, we propose a collision-free algorithm that can solve the problem with explicit termination. Thus, our algorithm is optimal with respect to the number of light colors. In addition, to the best of our knowledge, this paper is the first to report research considering (a variant of) uniform deployment in graphs other than rings or grids., 2021 Ninth International Symposium on Computing and Networking, CANDAR 2021, 23-26 November, 2021, Virtual Conference

We study a novel graph path planning problem for multiple agents that may crash at runtime, and block part of the workspace. In our setting, agents can detect neighboring crashed agents, and change followed paths at runtime. The objective is then to prepare a set of paths and switching rules for each agent, ensuring that all correct agents reach their destinations without collisions or deadlocks, despite unforeseen crashes of other agents. Such planning is attractive to build reliable multi-robot systems. We present problem formalization, theoretical analysis such as computational complexities, and how to solve this offline planning problem., to be presented at AAAI-23

We consider the gathering problem for asynchronous and oblivious robots that cannot communicate explicitly with each other, but are endowed with visibility sensors that allow them to see the positions of the other robots. Most of the investigations on the gathering problem on the discrete universe are done on ring shaped networks due to the number of symmetric configuration. We extend in this paper the study of the gathering problem on torus shaped networks assuming robots endowed with local weak multiplicity detection. That is, robots cannot make the difference between nodes occupied by only one robot from those occupied by more than one robots unless it is their current node. As a consequence, solutions based on creating a single multiplicity node as a landmark for the gathering cannot be used. We present in this paper a deterministic algorithm that solves the gathering problem starting from any rigid configuration on an asymmetric unoriented torus shaped network., Comment: 41 pages

The notions of scientific community and research field are central elements for researchers and the articles they publish. We propose to explore the evolution of the FUN conference community since its creation from the articles listed in DBLP, authors, program committees, and advertised themes, by means of a novel symmetric embedding, and carefully crafted software tools. Our results make it possible on the one hand to better understand the evolution of the community, and on the other hand to easily integrate new themes or researchers during future editions., LIPIcs, Vol. 226, 11th International Conference on Fun with Algorithms (FUN 2022), pages 21:1-21:13

International audience; This announces the first successful attempt at using model-checking techniques to verify the correctness of self-stabilizing distributed algorithms for robots evolving in a continuous environment. The study focuses on the problem of rendezvous of two robots with lights and presents a generic verification model for the SPIN model checker. It will be presented in full at an upcoming venue.

The vast majority of existing Distributed Computing literature about mobile robotic swarms considers computability issues: characterizing the set of system hypotheses that enables problem solvability. By contrast, the focus of this work is to investigate complexity issues: obtaining quantitative results about a given problem that admits solutions. Our quantitative measurements rely on a newly developed simulation framework to benchmark pen and paper designs. First, we consider the maximum traveled distance when gathering robots at a given location, not known beforehand (both in the two robots and in the n robots settings) in the classical OBLOT model, for the FSYNC, SSYNC, and ASYNC schedulers. This particular metric appears relevant as it correlates closely to what would be real world fuel consumption. Then, we introduce the possibility of errors in the vision of robots, and assess the behavior of known rendezvous (aka two robots gathering) and leader election protocols when sensors are unreliable. We also introduce two new algorithms, one for fuel efficient convergence, and one for leader election, that operate reliably despite unreliable sensors.

Self-stabilizing protocols enable distributed systems to recover correct behavior starting from any arbitrary configuration. In particular, when processors communicate by message passing, fake messages may be placed in communication links by an adversary. When the number of such fake messages is unknown, self-stabilization may require huge resources: generic solutions (a.k.a. data link protocols) require unbounded resources, which makes them unrealistic to deploy, specific solutions (e.g., census or tree construction) require O(n log n) or O(∆ log n) bits of memory per node, where n denotes the network size and ∆ its maximum degree, which may prevent scalability. We investigate the possibility of resource efficient self-stabilizing protocols in this context. Specifically, we present a self-stabilizing protocol for (∆+1)-coloring in any n-node graph, under the asynchronous message-passing model. The problem of (∆+1)-coloring is considered a benchmarking problem for local tasks. Our protocol offers many desirable features. It is deterministic, it converges in O(k∆n^2 log n) message exchanges, where k is the bound of the link capacity in terms of number of messages, and it uses messages on O(log log n+log ∆) bits with a memory of O(∆ log ∆+log log n) bits at each node. The resource consumption of our protocol is thus almost oblivious to the number of nodes, enabling scalability. Moreover, a striking property of our protocol is that the nodes do not need to know the number, or any bound on the number of messages initially present in each communication link of the initial (potentially corrupted) network configuration. This permits our protocol to handle any future network with unknown message capacity communication links. A key building block of our coloring scheme is a spanning directed acyclic graph construction, that is of independent interest, and can serve as a useful tool for solving other tasks in this challenging setting.

International audience; The paper details the first successful attempt at using model checking techniques to verify the correctness of distributed algorithms for robots evolving in a continuous environment. The study focuses on the problem of rendezvous of two robots with lights.There exist many different rendezvous algorithms that aim at finding the minimal number of colors needed to solve rendezvous in various synchrony models (e.g., FSYNC, SSYNC, ASYNC). While these rendezvous algorithms are typically very simple, their analysis and proof of correctness tend to be extremely complex, tedious, and error-prone as impossibility results are based on subtle interactions between the activation schedules of the robots.The paper presents a generic verification model that can be concretely expressed in available software model-checkers. In particular, we explain the subtle design decisions that allow to keep the search space finite and tractable, as well as prove several important theorems that support them. As a sanity check, we use the model to verify several known rendezvous algorithms in six different models of synchrony. In each case, we find that the results obtained from the model checker are consistent with the results known in the literature. The model checker outputs a counter-example execution in every case that is known to fail.In the course of developing and proving the validity of the model, we identified several fundamental theorems, including the ability for a well chosen algorithm and ASYNC scheduler to produce an emerging property of memory in a system of oblivious mobile robots, and why it is not a problem when robots executing the gathering algorithms are equipped with lights.