Livesey, Joseph and Wojtczak, Dominik ORCID: 0000-0001-5560-0546
(2021)
Propositional Gossip Protocols.
.
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) |
---|---|
Uncontrolled Keywords: | 4606 Distributed Computing and Systems Software, 46 Information and Computing Sciences, 4602 Artificial Intelligence |
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: | 20 Jun 2024 20:24 |
DOI: | 10.1007/978-3-030-86593-1_25 |
Related URLs: | |
URI: | https://livrepository.liverpool.ac.uk/id/eprint/3143420 |