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.
@article{arxiv.2202.11570,
title = {Monitoring hyperproperties with circuits},
author = {Luca Aceto and Antonios Achilleos and Elli Anastasiadi and Adrian Francalanza},
journal= {arXiv preprint arXiv:2202.11570},
year = {2022}
}
Comments
10 pages, 1 tikz figure, 1 table of semantics, accepted for FORTE 2022