Monitoring hyperproperties with circuits

TL;DR

This paper introduces a new circuit-based monitoring framework for hyperproperties, extending logic and providing a synthesis procedure for sound and violation-complete monitors over infinite traces.

Contribution

It develops a novel circuit-like monitor architecture and a synthesis method from logic formulae, enabling effective monitoring of hyperproperties.

Findings

Monitors are sound and violation complete.

The synthesis procedure produces correct circuit-like monitors.

Applicable to finite sets of infinite traces.

Abstract

This paper presents an extension of the safety fragment of Hennessy-Milner Logic with recursion over sets of traces, in the spirit of Hyper-LTL. It then introduces a novel monitoring setup that employs circuit-like structures to combine verdicts from regular monitors. The main contribution of this study is the monitors and their semantics themselves, as well as a monitor-synthesis procedure from formulae in the logic that yields `circuit-like monitors' of this type that are sound and violation complete over a finite set of infinite traces.