Model checking gossip modalities

We present a model checking technique for LRT, a temporal logic for communicating sequential agents (CSAs) introduced by Lodaya, Ramanujam, and Thiagarajan. LRT contains temporal modalities indexed with a local point of view of one agent and allows to refer to properties of other agents according to the latest gossip which is related to local knowledge. The model checking procedure relies on a modularisation of LRT into temporal and gossip modalities. We introduce a hierarchy of formulae and a corresponding hierarchy of equivalences, which allows to compute for each formula and finite state distributed system a finite multi modal Kripke structure, on which the formula can be checked with standard techniques