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.