Reasoning about Layered Message Passing Systems

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