Propositional Gossip Protocols
Gossip protocols are programs that can be used by a group of agents to synchronize what they know. Namely, assuming each agent holds a secret, the goal of a protocol is to reach a situation in which all agents know all secrets. Distributed epistemic gossip protocols use epistemic formulas in the component programs for the agents. We investigate open problems regarding the simplest class of gossip protocols: propositional ones, in which whether an agent wants to make a call depends only on their currently known set of secrets. Specifically, we show that all correct propositional gossip protocols, i.e., ones that always terminate in a situation where all agents knows all secrets, require the communication graph to be complete, whilst investigating the minimum number of calls required. We also investigate the complexity of the problem of checking correctness of a given propositional gossip protocol, before discussing implementing such a check with model checker NuSMV.