Verification of Distributed Epistemic Gossip Protocols

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 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').

To discuss these protocols we introduce an appropriate epistemic logic. Its semantics and its truth relation turn out to be decidable. This implies that the epistemic distributed gossip protocols are implementable and that their partial correctness, termination and two forms of fair termination are decidable.

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/1606.07516 and https://jair.org/index.php/jair/article/view/11204

hosted by

social