On decidability of a logic of gossips
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, see, e.g., . In , building upon , we studied distributed epistemic gossip protocols, which are examples of knowledge based programs introduced in . These protocols use as guards formulas from a simple epistemic logic. We show here that these protocols are implementable by proving that it is decidable to determine whether a formula with no nested modalities is true after a sequence of calls. Building upon this result we further show that the problems of partial correctness and of termination of such protocols are decidable, as well.
|Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|European Conference on Logics in Artificial Intelligence|
Apt, K.R, & Wojtczak, D.K. (2016). On decidability of a logic of gossips. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence. doi:10.1007/978-3-319-48758-8_2