Propositional Gossip Protocols



Livesey, Joseph and Wojtczak, Dominik ORCID: 0000-0001-5560-0546
(2021) Propositional Gossip Protocols. .

[img] Text
Joe_Gossip_Paper.pdf - Author Accepted Manuscript

Download (298kB) | Preview

Abstract

Gossip protocols are programs that can be used by a group of n agents to synchronise 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. In this paper, we solve open problems regarding one of the simplest classes of such gossip protocols: propositional gossip protocols, in which whether an agent can make a call depends only on his currently known set of secrets. Specifically, we show that all correct propositional gossip protocols, i.e., the ones that always terminate in a situation where all agents know all secrets, require the underlying undirected communication graph to be complete and at least 2 n- 3 calls to be made. We also show that checking correctness of a given propositional gossip protocol is a co-NP-complete problem. Finally we report on implementing such a check with model checker nuXmv.

Item Type: Conference or Workshop Item (Unspecified)
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 18 Nov 2021 11:13
Last Modified: 18 Jan 2023 21:24
DOI: 10.1007/978-3-030-86593-1_25
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3143420