Monitoring hyperproperties with circuits

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 s...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2022-05
Main Authors: Aceto, Luca, Achilleos, Antonios, Anastasiadi, Elli, Francalanza, Adrian
Format: Article
Language:English
Subjects:
Circuits
Monitoring
Monitors
Semantics
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422