Papers With

← All papers
First page of Self-Correcting Gossip Protocols

Self-Correcting Gossip Protocols

Giorgio Cignarale, Hans van Ditmarsch, Stephan Felber, Malvin Gattinger, Hugo Rincon Galeana, Vaishnavi Sundararajan

cs.LO May 7, 2026 · v1 cs.DC
formalization logic mathlib
Read PDF arXiv abstract Code
TL;DR
The semantics of self-correcting gossip is formalized in Lean 4 with Mathlib, proving well-foundedness of the evaluation and properties of knowledge and the observation relation.
Abstract
We investigate self-correcting gossip protocols with errors. In distributed computing, protocols with errors have been widely investigated in temporal epistemic logics. Instead, we propose a dynamic epistemic logic. We show how to correct transmission errors due to faulty messages without a central authority coordinating protocol execution, how this affects optimality, and how this compares to bounded memory and full information protocols.
Problem

Epistemic gossip protocols usually assume error-free message transmission. The paper asks which epistemic goals remain reachable when one transmission error may occur, and how optimality is affected without a central coordinating authority.

Approach

A dynamic epistemic logic is defined over secret distributions and call sequences containing at most one faulty call, with an observation relation and satisfaction semantics. It is compared with bounded-memory (last-call) and full-information call semantics. The mutually recursive definitions are formalized in Lean 4 using Mathlib. Lean is used to show that the evaluation function terminates under a lexicographic order.

Results

The work shows how agents can self-correct faulty secret values and how this affects the optimal number of calls. The Lean formalization verifies well-foundedness of the semantics, proves that the observation relation is an equivalence relation, and proves properties of knowledge and belief.