ACG

Verification of Distributed Epistemic Gossip Protocols (2)

Gossip protocols are concerned with the spread of knowledge in a social network. They aim at arriving, by means of point-to-point or group communications, at a situation in which all agents know each other's secrets.

We consider distributed gossip protocols that are expressed in a simple programming language that employs epistemic logic (for instance in statements such as `if I do not know whether agent i knows my secret I communicate it to him'). They are examples of so-called knowledge-based programs.

To discuss these protocols we introduce an appropriate epistemic logic and its semantics. These distributed epistemic gossip protocols are implementable and their partial correctness, termination, and two forms of fair termination are decidable.

We also analyze various forms of communication and their impact on the agents' knowledge, and discuss some open problems.

The talk is based on joint works with Davide Grossi, Wiebe van der Hoek, and Dominik Wojtczak. The relevant references can be found at https://arxiv.org/abs/1907.09097 , https://arxiv.org/abs/1807.05283 , and https://jair.org/index.php/jair/article/view/11204

Other presentations

hosted by

social