Centralized vs Decentralized Monitors for Hyperproperties

This paper focuses on the runtime verification of hyperproperties expressedin Hyper-recHML, an expressive yet simple logic for describing properties ofsets of traces. To this end, we consider a simple language of monitors thatobserve sets of system executions and report verdicts w.r.t. a givenHyper-recHML formula. We first employ a unique omniscient monitor thatcentrally observes all system traces. Since centralised monitors are not idealfor distributed settings, we also provide a language for decentralizedmonitors, where each trace has a dedicated monitor; these monitors yield aunique verdict by communicating their observations to one another. For both thecentralized and the decentralized settings, we provide a synthesis procedurethat, given a formula, yields a monitor that is correct (i.e., sound andviolation complete). A key step in proving the correctness of the synthesis fordecentralized monitors is a result showing that, for each formula, thesynthesized centralized monitor and its corresponding decentralized one areweakly bisimilar for a suitable notion of weak bisimulation.