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., [11]. In [1], building upon [3], we studied distributed epistemic gossip protocols, which are examples of knowledge based programs introduced in [6]. 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