  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.
