Centralized vs Decentralized Monitors for Hyperproperties
<|reference_start|>Centralized vs Decentralized Monitors for Hyperproperties: This paper focuses on the runtime verification of hyperproperties expressed in HypermuHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we first consider a simple language of monitors that can observe sets of system executions and report verdicts w.r.t. a given HypermuHML formula. In this setting, a unique omniscient monitor observes all system traces, and, in this sense, it is 'centralized'. However, in a possibly distributed system, having a centralized entity is undesirable; hence, we also provide a language for 'decentralized' monitors, where each trace has its own monitor, and monitors for different traces can yield a unique verdict by communicating their observations. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation.<|reference_end|>
@article{aceto2024centralized,
    title={Centralized vs Decentralized Monitors for Hyperproperties},
    author={Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza,
  Daniele Gorla, Jana Wagemaker},
    journal={arXiv preprint arXiv:2405.12882},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.12882},
    primaryClass={cs.LO}
}