A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring

Runtime verification aims at extracting information from a running system, and using it to detect and possibly react to behaviors violating a given correctness property. Decentralized runtime verification involves a set of monitors observing the behavior of the underlying system. When the monitors themselves can fail, and communication among them is unreliable, it is unavoidable that the monitors may have different views of the system’s state and hence that they emit different opinions about its correctness at runtime. It is known that few correctness properties can be monitored in such a setting, when the set of opinions is the set {True, False}. In this paper, we initiate the investigation of decentralized fault-tolerant runtime monitoring under an arbitrary set of opinions. Specifically, we characterize the size of the opinion set required for monitoring a given correctness property in a decentralized manner. It turns out that the key factor impacting this size is the maximum number of times the monitored property can change its truth value over all executions of the monitors. Our lower bound is independent of the way the set of opinions returned by the monitors is globally interpreted, and it holds even when verifying a static system. Moreover, our lower bound is tight in the sense that we design a distributed protocol enabling any given set of monitors to verify any given correctness property on static systems, using as many different opinions as the one given by our lower bound.