Efficient decentralized monitoring of safety in distributed systems

We describe an efficient decentralized monitoring algorithm that monitors a distributed program´s execution to check for violations of safety properties. The monitoring is based on formulae written in PT-DTL, a variant of past time linear temporal logic that we define. PT-DTL is suitable for expressing temporal properties of distributed systems. Specifically, the formulae of PT-DTL are relative to a particular process and are interpreted over a projection of the trace of global states that represents what that process is aware of. A formula relative to one process may refer to other processes´ local states through remote expressions and remote formulae. In order to correctly evaluate remote expressions, we introduce the notion of Knowledge Vector and provide an algorithm which keeps a process aware of other processes´ local states that can affect the validity of a monitored PT-DTL formula. Both the logic and the monitoring algorithm are illustrated through a number of examples. Finally, we describe our implementation of the algorithm in a tool called DIANA.