Epistemic Gossip Protocols



Attamah, MK
(2015) Epistemic Gossip Protocols. Doctor of Philosophy thesis, Unibversity of Liverpool.

[img] Text
200830864_Dec2015.pdf - Unspecified

Download (2MB)

Abstract

In this thesis we study epistemic protocols for gossip. Each agent in the gossip scenario knows a unique piece of information which is called a secret. Agents communicate with each other by means of pairwise telephone calls, and in each call the calling pair of agents exchange all the secrets they currently know. In an epistemic gossip protocol, an agent $a$ can call another agent $b$, not because it is so instructed, but because agent $a$ knows that it satisfies some knowledge-based condition defined by the protocol. The goal of gossiping is typically epistemic, for example, that after a sequence of calls, every agent knows the secret of every other agent. The question then arises as to which knowledge conditions bring about the goal of gossiping, and what properties the resulting protocols have. In this thesis we describe a theoretical framework for the study of epistemic gossip protocols based on dynamic epistemic logic. We describe a number of epistemic gossip protocols and formalise these protocols using our theoretical framework. We study and prove the dynamic properties of these protocols in various types of underlying network topologies such as the line topology network, circle topology network, tree topology network, and the complete topology network. Based on our theoretical framework, we implement a software framework for describing, modelling and checking the dynamic properties of epistemic gossip protocols. We call this software framework the Epistemic Gossip Protocol (EGP) tool. The EGP tool automates the checking of dynamic properties of a given epistemic gossip protocol, such as, whether the given protocol achieves the goal of gossiping for every execution sequence of the protocol, whether the given protocol can produce execution sequences that lead to a deadlock, or whether the given protocol can produce an infinite execution sequence due to a loop. We describe the details of the implementation of the EGP tool, and use the tool to model, and check the dynamic properties of our example protocols. We present and discuss the results obtained from our experiments with the EGP tool.

Item Type: Thesis (Doctor of Philosophy)
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 01 Aug 2016 09:37
Last Modified: 15 Apr 2021 07:14
DOI: 10.17638/03001317
Supervisors:
  • van der Hoek, W
  • Grossi, D
  • van Ditmarsch, H
URI: https://livrepository.liverpool.ac.uk/id/eprint/3001317