Centralized vs Decentralized Monitors for Hyperproperties
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918004845969408 |
|---|---|
| author | Aceto, Luca Achilleos, Antonis Anastasiadi, Elli Francalanza, Adrian Gorla, Daniele Wagemaker, Jana |
| author_facet | Aceto, Luca Achilleos, Antonis Anastasiadi, Elli Francalanza, Adrian Gorla, Daniele Wagemaker, Jana |
| contents | This paper focuses on the runtime verification of hyperproperties expressed in Hyper-recHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-recHML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralised monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_12882 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Centralized vs Decentralized Monitors for Hyperproperties Aceto, Luca Achilleos, Antonis Anastasiadi, Elli Francalanza, Adrian Gorla, Daniele Wagemaker, Jana Logic in Computer Science F.3.1 This paper focuses on the runtime verification of hyperproperties expressed in Hyper-recHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-recHML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralised monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. 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. |
| title | Centralized vs Decentralized Monitors for Hyperproperties |
| topic | Logic in Computer Science F.3.1 |
| url | https://arxiv.org/abs/2405.12882 |