TY - CHAP
T1 - Monitoring Hyperproperties with Circuits
AU - Aceto, Luca
AU - Anastasiadi, Elli
AU - Francalanza, Adrian
N1 - Funding Information: The authors were supported by the projects ‘Open Problems in the Equational Logic of Processes’ (OPEL) (grant No 196050–051) and ‘Mode(l)s of Verification and Monitora-bility’ (MoVeMent) (grant No 217987) of the Icelandic Research Fund, and ‘Runtime and Equational Verification of Concurrent Programs’ (ReVoCoP) (grant No 222021), of the Reykjavik University Research Fund. Luca Aceto’s work was also partially supported by the Italian MIUR PRIN 2017 project FTXR7S IT MATTERS ‘Methods and Tools for Trustworthy Smart Systems’. Publisher Copyright: © 2022, IFIP International Federation for Information Processing.
PY - 2022
Y1 - 2022
N2 - 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 definition of the monitors and their semantics, as well as a monitor-synthesis procedure from formulae in the logic that yields ‘circuit-like monitors’ that are sound and violation complete over a finite set of infinite traces.
AB - 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 definition of the monitors and their semantics, as well as a monitor-synthesis procedure from formulae in the logic that yields ‘circuit-like monitors’ that are sound and violation complete over a finite set of infinite traces.
UR - https://www.scopus.com/pages/publications/85133004594
U2 - 10.1007/978-3-031-08679-3_1
DO - 10.1007/978-3-031-08679-3_1
M3 - Chapter
SN - 9783031086786
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 10
BT - Formal Techniques for Distributed Objects, Components, and Systems - 42nd IFIP WG 6.1 International Conference, FORTE 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Proceedings
A2 - Mousavi, Mohammad Reza
A2 - Philippou, Anna
PB - Springer Science and Business Media Deutschland GmbH
T2 - 42nd IFIPWG6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2022 Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022
Y2 - 13 June 2022 through 17 June 2022
ER -