Verification of Distributed Epistemic Gossip Protocols
Abstract
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.
Cite
Text
Apt and Wojtczak. "Verification of Distributed Epistemic Gossip Protocols." Journal of Artificial Intelligence Research, 2018. doi:10.1613/JAIR.1.11204Markdown
[Apt and Wojtczak. "Verification of Distributed Epistemic Gossip Protocols." Journal of Artificial Intelligence Research, 2018.](https://mlanthology.org/jair/2018/apt2018jair-verification/) doi:10.1613/JAIR.1.11204BibTeX
@article{apt2018jair-verification,
title = {{Verification of Distributed Epistemic Gossip Protocols}},
author = {Apt, Krzysztof R. and Wojtczak, Dominik},
journal = {Journal of Artificial Intelligence Research},
year = {2018},
pages = {101-132},
doi = {10.1613/JAIR.1.11204},
volume = {62},
url = {https://mlanthology.org/jair/2018/apt2018jair-verification/}
}