Propositional Gossip Protocols



Livesey, Joseph
(2023) Propositional Gossip Protocols. PhD thesis, University of Liverpool.

[img] Text
201385346_Apr2023.pdf - Author Accepted Manuscript

Download (1MB) | Preview

Abstract

Gossip protocols are programs which can be used by a group of agents to synchronise information which is known by each. We assume each agent holds a unique piece of information which is known as a secret, with the goal of the protocol to reach a situation where all agents are experts, i.e. where each agent knows every secret. Distributed epistemic gossip protocols use epistemic formulas in the component programs for the agents. In this thesis we shall study one of the simplest classes of such protocols: propositional gossip protocols, in which the calls made by agents are determined only by the set of secrets the agent currently knows. Propositional gossip protocols are simple and quick to execute, due to their guards being evaluated in linear time, making them potentially well suited for small devices with limited memory and computational capabilities. This raises many natural questions about conditions necessary for a propositional gossip protocol to be correct, i.e. always terminated in the all-expert state. In this thesis we shall show that such a protocol can be correct only if for any two agents, at least one of them can call the other at some stage in the protocol. In other words, the underlying undirected communication graph must be complete. Furthermore, we shall show that for any such protocol with n ≥ 4 agents, at least 2n − 2 calls are required in the worst case. We continue to study the complexity of checking the correctness of such a protocol, as well as the related sub problems of termination and partial correctness, showing that these are coNP-complete problems. We move on to show how this characterization changes when fairness constraints are imposed on the call scheduler used, showing that many more protocols of different structures become viable, as the requirement of the underlying undirected communication graph to be complete is no longer necessary. We continue again to investigate the complexity of checking the correctness of these protocols with fair schedulers, showing the problem of correctness again to be coNP-complete. Finally, we shall look at the topic of simulation, in which we look at if two propositional gossip protocols can have such similarities that one may be able to replicate all call sequences from the other. This could allow for seemingly more complex protocols to be replaced with less computationally demanding protocols, whilst achieving the same results. We find that the problem of checking if a protocol may simulate another protocol is coNP-complete.

Item Type: Thesis (PhD)
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 14 Aug 2023 15:00
Last Modified: 14 Aug 2023 15:00
DOI: 10.17638/03170190
Supervisors:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3170190