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

Slides: [Part 1]

• Epistemic Logic for Gossip
• Strengthening of protocols
• Implementing strengthening in GoMoChe
• The logic of protocol-dependent knowledge

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

Slides: [Part 1]

• 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 (Solved, discussed Wednesday.)

Suppose agents do not know who calls them, but still exchange all secrets they know in a call. Also assume we have at least four agents, that no protocol is known among the agents and that we are in an asynchronous setting.

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, try to redefine epistemic indistinguishability.)

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.

Note: The description above has been clarified a bit, as discussed on Wednesday. For alternative versions of the puzzle, assume that even the caller does not know who the callee is, and also consider the synchronous setting.

Puzzle 2: Can you find the bug?

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

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!