Monitoring Hyperproperties over Observed and Constructed Traces
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911090537922560 |
|---|---|
| author | Chalupa, Marek Henzinger, Thomas A. da Costa, Ana Oliveira |
| author_facet | Chalupa, Marek Henzinger, Thomas A. da Costa, Ana Oliveira |
| contents | We study the problem of monitoring at runtime whether a system fulfills a specification defined by a hyperproperty, such as linearizability or variants of non-interference. For this purpose, we introduce specifications with both passive and active quantification over traces. While passive trace quantifiers range over the traces that are observed, active trace quantifiers are instantiated with \emph{generator functions}, which are part of the specification. Generator functions enable the monitor to construct traces that may never be observed at runtime, such as the linearizations of a concurrent trace. As specification language, we extend hypernode logic with trace quantifiers over generator functions and interpret these hypernode formulas over possibly infinite domains. We present a corresponding monitoring algorithm, which we implemented and evaluated on a range of hyperproperties for concurrency and security applications. Our method enables, for the first time, the monitoring of asynchronous hyperproperties that contain alternating trace quantifiers. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_02301 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Monitoring Hyperproperties over Observed and Constructed Traces Chalupa, Marek Henzinger, Thomas A. da Costa, Ana Oliveira Logic in Computer Science 68Q60, 68Q45 F.3.1; D.3.1 We study the problem of monitoring at runtime whether a system fulfills a specification defined by a hyperproperty, such as linearizability or variants of non-interference. For this purpose, we introduce specifications with both passive and active quantification over traces. While passive trace quantifiers range over the traces that are observed, active trace quantifiers are instantiated with \emph{generator functions}, which are part of the specification. Generator functions enable the monitor to construct traces that may never be observed at runtime, such as the linearizations of a concurrent trace. As specification language, we extend hypernode logic with trace quantifiers over generator functions and interpret these hypernode formulas over possibly infinite domains. We present a corresponding monitoring algorithm, which we implemented and evaluated on a range of hyperproperties for concurrency and security applications. Our method enables, for the first time, the monitoring of asynchronous hyperproperties that contain alternating trace quantifiers. |
| title | Monitoring Hyperproperties over Observed and Constructed Traces |
| topic | Logic in Computer Science 68Q60, 68Q45 F.3.1; D.3.1 |
| url | https://arxiv.org/abs/2508.02301 |