Verification of distributed epistemic gossip protocols
Journal of Artificial Intelligence Research , Volume 62 p. 101- 132
Gossip protocols aim at arriving, by means of point-to-point or group communications, at a situation in which all the agents know each other secrets. Distributed epistemic gossip protocols use as guards formulas from a simple epistemic logic and as statements calls between the agents. They are natural examples of knowledge based programs.
We prove here that these protocols are implementable, that their partial correctness is decidable and that termination and two forms of fair termination of these protocols are decidable, as well. To establish these results we show that the definition of semantics and of truth of the underlying logic are decidable.
|Journal of Artificial Intelligence Research|
|Organisation||Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands|
Apt, K.R, & Wojtczak, D.K. (2018). Verification of distributed epistemic gossip protocols. Journal of Artificial Intelligence Research, 62, 101–132.
|View at publisher Final Version|