Lamport diagrams are partial orders which depict computations of message passing systems. It is natural to consider generalizations
of linear time temporal logics over such diagrams. In [MR00], we presented a decidable temporal logic with local temporal
modalities and a global ‘previous’ modality to talk of message receipts. It seems reasonable to extend the logic with a global
‘next’ modality as well, so that sending of messages may also be easily specified, but this (or other similar attempts) lead
to undecidability. Hence we consider ways of restricting the models so as to obtain decidability, while retaining the expressiveness
of global ‘next’ and global ‘previous’ modalities. For this, we consider Lamport diagrams presented as a sequence of layers. The layers themselves describe finite communication patterns and a diagram is obtained by sequential composition of such
parallel processes. The logic is defined appropriately, with layer formulas describing processes within a layer, and temporal
formulas describing the sequence of layers in the computation. When the number of events in layers is uniformly bounded and
each layer is communication closed, we get decidability. Alternatively, a stronger uniform bound on what we term channel capacity
also yields decidability. We present an example of system specification in the logic.