The logic of Gossiping

International audienceThe so-called gossip problem is a formal model of peer-to-peer communication. In order to perform such communication efficiently, it is important to keep track of what agents know about who holds what information at a given point in time. The knowledge that the agents possess depends strongly on the particular type of communication that is used.Here, we formally define a large number of different variants of the gossip problem, that differ in the extent to which communication is private (observable, synchronous or asynchronous), the direction of the flow of information (caller to callee, callee to caller or both) and whether the agents become aware of the exact set of information possessed by their communication partner.We consider a number of formulas that represent interesting properties that a gossip situation may or may not enjoy, and show for which variants they are valid. Additionally, we show that the model checking and validity checking problems for each variant are decidable, and we introduce sound and complete proof systems for them