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.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:706695 |
| Date | January 2015 |
| Creators | Attamah, M. K. |
| Publisher | University of Liverpool |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://livrepository.liverpool.ac.uk/3001317/ |
Page generated in 0.0141 seconds