A Distance Realization problem asks, given an n× n matrix D of nonnegative integers, to find an n-vertex graph G and an integral weight function on the edges realizing D, i.e., such that dist_G(i,j) , the weighted distance from i to j, equals D_i,j for every i and j, or decide that no such realizing graph exists. This paper introduces and studies the Minimum Deviation Distance Realization optimization problem, where given a matrix D, the goal is to find a weighted graph (G, w) that realizes D as closely as possible, i.e., such that the deviation ϕ (D,G) between D and the matrix of pairwise distances in G is minimized. We focus on four different types of deviation functions ϕ : the maximum difference over all matrix entries, ϕ _max , the sum of differences of all matrix entries, ϕ _sum , the number of matrix entries exhibiting a mismatch, ϕ _num , and the multiplicative difference over all matrix entries, ϕ _mult . For each deviation function ϕ , we consider the following variants of minimum deviation distance realization problems: (i) The deviation of the realizing graph (G, w) from the matrix D is allowed to be only upwards, only downwards, or in both directions; and (ii) The entries of D may specify exact values or ranges of permissible values. For each problem in this wide spectrum of variants, we either present a polynomial-time algorithm or show hardness and give a polynomial-time approximation algorithm.
In this paper, we consider the uniform deployment problem of myopic luminous robots in rings, requiring them to spread uniformly in the ring. Robots are myopic if they have a common limited visibility range and robots are luminous if hey are equipped with a light device that can emit a color from a finite set. The past related research considered uniform deployment for myopic and oblivious robots. Here, robots are oblivious if they have no memory and cannot memorize the history of past actions. In this case, it is shown that quiescent uniform deployment, requiring that robots stop moving after they reached a uniformly deployed configuration but they are allowed to resume moving when observing some configuration changes, is impossible. In this paper, we consider the feasibility of the uniform deployment problem by introducing lights. Let n be the number of nodes and k be the number of robots. First, we show that, even if robots behave fully synchronously and have an infinite number of light colors, they cannot achieve uniform deployment when either of the followings holds: (i) they do not have a common sense of direction, (ii) the visibility range is less than ⌊ n/k⌋ , or (iii) the problem requires explicit termination detection. Next, for robots that behave semi-synchronously and have a common sense of direction and visibility range at least ⌊ n/k⌋ , we propose an algorithm to solve the quiescent uniform deployment problem, by allowing robots to be luminous and have a constant number of light colors. This is a striking difference compared to the past result for oblivious robots.
Asynchronous executions of robotic swarm algorithms are challenging to reason about because they allow robots to compute their next destination based on observations that may be outdated. To add formal guarantees in such a context where subtle mistakes lead to dramatic errors, we propose a formalization for the Rocq prover of asynchronous executions in the Look-Compute-Move model, as an extension to the Pactole formal library, and we illustrate how algorithms can be proved correct in this setting. Intuition makes it easy to overlook crucial details that formal methods would request when used, leading to published algorithms which can be, at best, seriously underspecified. This is particularly the case when problems seem easy, as with solving Gathering using Weber points. Attempts at formalization show that going blindly (or for that matter cautiously) towards the Weber point, a strategy often claimed to solve Gathering, is indeed incorrect under certain assumptions. We propose in this work an original and formally certified algorithm for Gathering in async. As this algorithm uses Weber points, we also provide a comprehensive formalization for Weber points and their properties. Interestingly, the use of our formalization for asynchronous executions does not come with an explosion of the proof size, which stays at a very reasonable level.
Self-stabilization is a versatile methodology for designing fault-tolerant distributed algorithms for transient faults. Many self-stabilizing distributed algorithms adopt the state-reading model (or locally shared memory model), in which each process can read the local variables of its direct neighbor processes, in addition to its own local variables. In this paper, we propose a new model, named the R( d_r )W( d_w ) model. In this model, each process can read the local variables of processes within a distance of d_r ( ≥ 1 ) and write the local variables of processes within a distance of d_w ( ≥ 0 ). We present several self-stabilizing distributed algorithms in the proposed model. Furthermore, we present a transformer that directly simulates the R(1)W(1) model in the synchronous message passing model.
Epistemic Logic has been shown to provide a useful abstract framework for reasoning about fault tolerant distributed algorithms. In particular, it provides a way to derive protocols that are optimal in the way that they use information. An example of this is results using notions of common knowledge to establish the optimality of consensus protocols, under a variety of failure models. Proofs in this area have, to date, been performed manually, and have consequently been error-prone. This paper addresses this weakness using formal methods. A formalization in the theorem prover Isabelle is developed of a general framework for epistemic reasoning about distributed algorithms, that can cover multiple failure models and concrete protocols. As an application of the framework, it is formally proved that for all patterns of information exchange among the agents, the implementation of a knowledge based program is optimal among protocols for simultaneous consensus that use that pattern of information exchange. Furthermore, the FloodSet protocol has been modelled in our framework and we verified knowledge properties about the protocol.
