Efficient Decentralized Monitoring of Safety in Distributed Systems
Koushik Sen, Abhay Vardhan, Gul Agha, Grigore Roşu · 2004
This paper presents a variant of past time linear temporal logic, called PT-DTL, suitable for expressing temporal properties of distributed systems. The formulae in this logic are given with respect to a particular process and are interpreted over a trace of global states that the process is aware of. In a formula, a process can refer to other processes’ local states through remote expressions and remote formulae. We describe an efficient decentralized monitoring algorithm that checks whether a running distributed program satisfies a safety property expressed in PT-DTL. In order to correctly evaluate remote expressions, we introduce the notion of KNOWLEDGEVECTOR and give an algorithm which keeps a process aware of other processes ’ local states that can affect the validity of a monitored PT-DTL formula. An implementation of the algorithm in a tool DIANA is available to download. Both the logic and the monitoring algorithm are illustrated through a number of examples. 1