Gossip and Knowledge (ESSLLI 2025, Bochum)

Description

Gossip protocols facilitate peer-to-peer information sharing in networks. Each agent starts with some private information and the goal is to share this information among all agents. In distributed gossip, there is no central controller deciding who may call whom, but this is determined by independent pro-active agents and chance. In epistemic gossip protocols, knowledge conditions may restrict possible calls, for example you may avoid calling an agent who you know already to know your secret. In dynamic gossip, agents also exchange 'telephone numbers', leading to network expansion.

This course is based on the textbook "Reasoning about Gossip" by van Ditmarsch, to appear with Cambridge University Press. We will give a survey of results and methods in distributed epistemic gossip. Topics include constructing and revising gossip graphs, enumerating call sequences, and model checking gossip protocols. Next to the book we use software implementations of gossip protocols by Gattinger.

Main references

For the upcoming book Reasoning about Gossip, see reasoningaboutgossip.eu.

Schedule

Week 1 of ESSLLI 2025, 17:00-18:30 in room HGB 50.

Monday

Slides: [Part 1] [Part 2]

• Introduction
• ElmGossip

Main reference:

• Chapters 1 and 2 of Reasoning about Gossip

Classical References (in one PDF, collected by Torsten Sillke):

• Brenda Baker and Robert Shostak: Gossips and Telephones, Discrete Mathematics 2 (1972), 191-193.
• R. Tijdeman: On A Telephone Problem, Nieuw Archief voor Wiskunde (3), XIX (1971), 188-192.
• A. Hajnal, E. C. Milner and E. Szemerédi: A Cure For The Telephone Disease, Canad. Math. Bull. 15 (1972), 447–450.

Software:

• Ramon Meffert: ElmGossip: Explore dynamic gossip in your browser, 2021. [CODE] [Try it!]

Tuesday

Slides: [Part 1] [Part 2] [Part 3]

• Call Semantics
• Epistemic and distributed protocol conditions
• Gossip Model Checking with GoMoChe

Main reference:

• Chapters 2 and 3 of Reasoning about Gossip

Software:

• Malvin Gattinger: GoMoChe. [CODE] [Try it!]

Wednesday

Slides: [Part 1] [Part 2]

• Reachability
• Dynamic gossip

Reference:

• Chapters 5 and 6 of Reasoning about Gossip.
• Hans van Ditmarsch, Malvin Gattinger, Ioannis Kokkinis, Louwe B. Kuijer: Reachability of Five Gossip Protocols. RP2019 [PDF] [DOI]

Thursday

• Epistemic Logic for Gossip
• Strengthening of protocols
• Implementing strengthening in GoMoChe

References:

• Chapters 2 and 3 of Reasoning about Gossip

• Hans van Ditmarsch, Malvin Gattinger, Louwe B. Kuijer, Pere Pardo: Strengthening Gossip Protocols using Protocol-Dependent Knowledge. Applied Logics, 6 (1), 2019. [PDF]

Friday

• Epistemic Goals
• Unsatisfiability of higher-order knowledge
• Gossip in SMCDEL — a bug puzzle challenge

References:

• Chapter 11 of Reasoning about Gosisp.
• Hans van Ditmarsch and Malvin Gattinger: You can only be lucky once: optimal gossip for epistemic goals, Mathematical Structures in Computer Science, Volume 34, Issue 7, pp. 661-688, 2024. [PDF] [DOI]

Puzzles

You can win a t-shirt for solving each of the following two puzzles.

Puzzle 1: Anonymous Gossip

NOTE: This puzzle has been solved. We will discuss the answer at the end of the Wednesday lecture.

Suppose agents do not know whom they are talking to, but still exchange all secrets they know in a call. Also assume we have at least four agents.

As a warm-up, what do you then know if you call someone and they only tell you one secret? What if they tell you two? (Formally, we need to redefine epistemic indistinguishability of call sequences.)

Now the challenge: Can we still reach super success? That is, can we reach that everyone knows that everyone knows all the secrets? If yes, provide a call sequence that reaches the goal. If not, proof that there is none.

Puzzle 2: Can you find the bug?

In the lectures you have seen ElmGossip and GoMoChe, two programs However, there are also more generic model checkers for epistemic logics like DEMO-S5, MCK and SMCDEL. We can also model the gossip problem as a specific model for those programs, they might even be faster, depending on the approach. Of course, the different model checkers should agree on the results. Sadly, this is not the case between SMCDEL and GoMoChe, for this question:

With four agents (named 0 to 3), after calls 01 and 12 we expect agent 2 to know that agent 0 has secret 1, because 1 knows secret 0, and cannot have learned it via 3 because 1 does not know 3.

GoMoChe gives this result:

λ> (totalInit 4, parseSequence "01;12") |= K 2 anyCall (S 0 1)
True

But SMCDEL disagrees:

stack ghci src/SMCDEL/Examples/GossipS5.hs
λ> after 4 [(0,1),(1,2)] |= K "2" (PrpF $ hasSof 4 0 1)
False

As a warm-up, which of the two is correct?

Now the challenge: Can you find the bug hiding somewhere in this encoding of Gossip as symbolic transformers?

See also here and also feel free to ask further questions there!