We consider the problem of gathering in finite time and at the same location, not known beforehand, a set of deterministic semi-synchronous robots, starting from an arbitrary initial configuration that may even be bivalent (that is, a configuration where the robots are evenly split on two different locations). This problem is known to be unsolvable when the robots are oblivious, that is, when they cannot remember their past actions. We present two deterministic gathering algorithms where robots may remember and communicate a single bit of memory. This bit may be arbitrarily (and adversarially) set in the initial configuration. Our solutions are thus memory optimal and self-stabilizing. The first algorithm makes use of multiplicity detection, while the second solely uses robot colors. Their proof of correctness is formally certified by the Coq proof assistant using the Pactole framework.

This study examines a novel planning problem for multiple agents that cannot share holding resources, namedOffline Time-Independent Multiagent Path Planning (OTIMAPP). Given a graph and a set of start-goal pairs, the problem to be addressed is assigning a path to each agent, such that every agent eventually reaches its destination without blocking others, regardless of when each agent starts and finishes each own action. This motivation stems from timing uncertainties, including the reality gaps between planning and robot execution. In contrast to conventional solution, concepts of multirobot path planning that rely on timings, once OTIMAPP solutions are obtained, they can be executed without any synchronization between robot actions. Moreover, there is a theoretical guarantee that all robots eventually reach their destinations, provided they avoid interrobot collisions. This study attempts to establish OTIMAPP both theoretically and practically. Specifically, we present a formalization of the problem, solution conditions based on a categorization of deadlocks, computational complexities showing that OTIMAPP is computationally intractable, practical relaxation of the solution concept, two algorithms to solve OTIMAPP based on multiagent pathfinding algorithms, empirical results showing large OTIMAPP instances can be solved to some extent, as well as robot demonstrations of asynchronous OTIMAPP execution.

This paper studies a novel planning problem for multiple agents that cannot share holding resources, named OTIMAPP (Offline Time-Independent Multi-Agent Path Planning). Given a graph and a set of start-goal pairs, the problem consists in assigning a path to each agent such that every agent eventually reaches their goal without blocking each other, regardless of how the agents are being scheduled at runtime. The motivation stems from the nature of distributed environments that agents take actions fully asynchronous and have no knowledge about those exact timings of other actors. We present solution conditions, computational complexity, solvers, and robotic applications.

This article addresses novel real-valued consensus problems in the presence of malicious adversaries that can move within the network and induce faulty behaviors in the attacked agents. By adopting several mobile adversary models from the computer science literature, we develop protocols which can mitigate the influence of such malicious agents. The algorithms follow the class of mean subsequence reduced (MSR) algorithms, under which agents ignore the suspicious values received from neighbors during their state updates. Different from the static adversary models, even after the adversaries move away, the infected agents may remain faulty in their values, whose effects must be taken into account. We develop conditions on the network structures for both the complete and non-complete directed graph cases, under which the proposed algorithms are guaranteed to attain resilient consensus. The tolerance bound for network conditions becomes more strict as the adversaries are allowed to have more power. Extensive simulations are carried out over random graphs to verify the effectiveness of our approach when the information of the adversarial agents in terms of their models and numbers is unknown to the agents.

The paper proposes a new approach to model checking Chandy-Lamport Distributed Snapshot Algorithm (CLDSA). The essential of the approach is that CLDSA is specified as a meta-program in Maude such that the meta-program takes a specification of an underlying distributed system (UDS) and generates the specification of the UDS on which CLDSA is superimposed (UDS-CLDSA). To model check that a UDS-CLDSA enjoys a desired property, it suffices that human users specify the UDS for the proposed approach, while human users need to specify the UDS-CLDSA for the existing approach for each UDS. Since the proposed approach conducts model checking at meta-level, it produces a counterexample if a UDS-CLDSA does not enjoy the property, while the existing approach does not. Our method specifying CLDSA as a meta-program can be applied to formal specification of the class of distributed algorithms that are superimposed on UDSs.

Recent advances in distributed computing highlight models and algorithms for autonomous mo- bile robots that self-organize and cooperate together in order to solve a global objective. As results, a large number of algorithms have been proposed. These algorithms are given together with proofs to assess their correctness. However, those proofs are informal, which are error prone. This paper presents our study on formal verification of mobile robot algorithms. We first propose a formal model for mobile robot algorithms on anonymous ring shape network under multiplicity and asynchrony assumptions. We specify this formal model in Maude, a specification and pro- gramming language based on rewriting logic. We then use its model checker to formally verify an algorithm for robot gathering problem on ring enjoys some desired properties. As the result of the model checking, counterexamples have been found. We detect the sources of some unforeseen design errors. We, furthermore, give our interpretations of these errors.

This article addresses the consensus problem in asynchronous systems prone to process crashes, where additionally the processes are anonymous (they cannot be distinguished one from the other: they have no name and execute the same code). To circumvent the three computational adversaries (asynchrony, failures, and anonymity) each process is provided with a failure detector of a class denoted ψ , that gives it an upper bound on the number of processes that are currently alive (in a nonanonymous system, the classes ψ and P ---the class of perfect failure detectors---are equivalent). The article first presents a simple ψ -based consensus algorithm where the processes decide in 2 t + 1 asynchronous rounds (where t is an upper bound on the number of faulty processes). It then shows one of its main results, namely 2 t + 1 is a lower bound for consensus in the anonymous systems equipped with ψ . The second contribution addresses early-decision. The article presents and proves correct an early-deciding algorithm where the processes decide in min(2 f + 2, 2 t + 1) asynchronous rounds (where f is the actual number of process failures). This leads us to think that anonymity doubles the cost (with respect to synchronous systems) and it is conjectured that min(2 f + 2, 2 t + 1) is the corresponding lower bound. The article finally considers the k -set agreement problem in anonymous systems. It first shows that the previous ψ -based consensus algorithm solves the k -set agreement problem in Rt = 2⌊t k⌋ + 1 asynchronous rounds. Then, considering a family of failure detector classes { ψℓ }0 ≤ ℓ < k that generalizes the class ψ (= ψ 0 ), the article presents an algorithm that solves the k -set agreement in Rt,ℓ = 2 ⌊ t k − ℓ ⌋ + 1 asynchronous rounds. This last formula relates the cost ( Rt,ℓ ) the coordination degree of the problem ( k ), the maximum number of failures ( t ), and the the strength ( ℓ ) of the underlying failure detector. Finally the article concludes by presenting problems that remain open.

This paper is on failure detectors to solve the consensus problem in asynchronous systems made up of anonymous processes prone to crash and connected by asynchronous reliable channels. Anonymity means that any two processes cannot be distinguished one from the other: they have no name and execute the same code. The paper has several contributions. It first introduces two new classes of failures detectors, denoted AP and AOmega, and presents an AP-based algorithm and an AOmega-based algorithm that solve the consensus problem despite the three computational adversaries that are asynchrony, failures and anonymity. Then, the paper shows that, in crash-prone non-anonymous systems, (a) AP and the class of perfect failure detectors denoted P) are equivalent, and (b) AOmega and the class of eventual leader failure detectors (denoted Omega) are also equivalent. Finally, the paper addresses the question of the weakest failure detector to solve consensus in an asynchronous crash-prone anonymous system. In non-anonymous systems, the class P of perfect failure detectors is strictly stronger than the class Omega of eventual leader failure detectors that has been shown to be the weakest failure detector class for consensus in asynchronous crash-prone system. Quite surprisingly, the paper shows that their anonymous counterparts cannot be compared.

This paper proposes the first study of the consensus problem in the anonymous crash-prone message-passing systems.

The k-set agreement problem is a generalization of the consensus problem: considering a system made up of n processes where each process proposes a value, each non-faulty process has to decide a value such that a decided value is a proposed value, and no more than k different values are decided. While this problem cannot be solved in an asynchronous system prone to t process crashes when t \geq k, it can always be solved in a synchronous system; \lfloor \frac{t}{k} \rfloor +1 is then a lower bound on the number of rounds (consecutive communication steps) for the non-faulty processes to decide. The {\it condition-based} approach has been introduced in the consensus context. Its aim was to both circumvent the consensus impossibility in asynchronous systems, and allow for more efficient consensus algorithms in synchronous systems. This paper addresses the condition-based approach in the context of the k-set agreement problem. It has two main contributions. The first is the definition of a framework that allows defining conditions suited to the \ell$-set agreement problem. More precisely, a condition is defined as a set of input vectors such that each of its input vectors can be seen as "encoding" \ell values, namely, the values that can be decided from that vector. A condition is characterized by the parameters t, \ell, and a parameter denoted d such that the greater d+\ell, the least constraining the condition (i.e., it includes more and more input vectors when d+\ell increases, and there is a condition that includes all the input vectors when d+\ell≫t$). The conditions characterized by the triple of parameters t, d and \ell define the class of conditions denoted ${\cal S}_t^{d,\ell}$, $0\leq d\leq t$, $1\leq \ell \leq n-1 $. The properties of the sets ${\cal S}_t^{d,\ell}$ are investigated, and it is shown that they have a lattice structure. The second contribution is a generic synchronous k-set agreement algorithm based on a condition $C\in {\cal S}_t^{d,\ell}$, i.e., a condition suited to the $\ell$-set agreement problem, for $\ell \leq k$. This algorithm requires at most $\left\lfloor \frac{d-1+\ell}{k} \right\rfloor +1$ rounds when the input vector belongs to $C$, and $\left\lfloor \frac{t}{k} \right\rfloor +1 rounds otherwise. (Interestingly, this algorithm includes as particular cases the classical synchronous k-set agreement algorithm that requires $\left\lfloor \frac{t}{k} \right\rfloor+1 rounds (case $d=t$ and $\ell=1$), and the synchronous consensus condition-based algorithm that terminates in d+1 rounds when the input vector belongs to the condition, and in t+1 rounds otherwise (case $k=\ell=1$).)

This BA extends the condition-based approach to the ll-set agreement problem.