Events

Distributed systems—from large-scale communication networks to swarms of simple mobile robots—must often verify or achieve global properties while each participant sees only its immediate surroundings. This talk presents two lines of work addressing this challenge.

The first part concerns /distributed local verification/. In large networks, one frequently needs to check that a computed structure—a spanning tree, a proper coloring, the absence of cycles—is actually correct, and to do so quickly, in a fault-tolerant and self-stabilizing manner, without any single node inspecting the whole system. Proof Labeling Schemes and Locally Checkable Proofs formalize this: a prover assigns short labels to nodes, and each node, seeing only its local neighborhood and nearby labels, decides whether to accept. We study the verification of cycle existence, cycle-freeness, and bipartiteness, and characterize the trade-off between proof size and view distance—showing, for instance, that cycle existence requires three labels at view distance one, yet only a single bit at view distance three via a carefully chosen non-palindromic gadget. We then extend these results to an adversarial setting in which a bounded number of proof labels may be corrupted, obtaining error-resilient verification schemes.

The second part turns to the coordination of autonomous mobile robots. Inspired by the collective behavior of biological swarms, a central question is whether a group of anonymous, identical robots with only local and limited knowledge can accomplish meaningful global tasks—a model directly relevant to low-cost robot swarms in exploration, coverage, and monitoring. Working with luminous robots that operate in Look-Compute-Move cycles under asynchronous schedulers, we present algorithms for several fundamental tasks: filling maximal independent sets and minimal vertex covers on graphs, and achieving mutual visibility in the plane despite angular inaccuracy, mobility faults, and the absence of a common coordinate system, along with uniform partitioning of a bounded region.