## 1 Introduction

## 2 Runtime verification of \(\text {HyperLTL}\)

### 2.1 HyperLTL

### 2.2 Monitorability

## 3 Monitoring hyperproperties in the parallel model

### 3.1 Finite trace semantics

### 3.2 Monitoring algorithms

#### 3.2.1 Online algorithm

#### 3.2.2 Offline algorithm

## 4 Monitoring hyperproperties in the sequential model

### 4.1 Optimizations

#### 4.1.1 Specification analysis

#### 4.1.2 Trace analysis

- Case \(T \in {\mathcal {H}}(\varphi )\), then \({T \subseteq {\mathcal {L}}({\mathcal {A}}_\varphi [t/\pi _1]) \subseteq {\mathcal {L}}({\mathcal {A}}_\varphi [t'/\pi _1])}\) and \(T \subseteq {\mathcal {L}}({\mathcal {A}}_\varphi [t/\pi _2]) \subseteq {\mathcal {L}}({\mathcal {A}}_\varphi [t'/\pi _2])\). By Lemma 4 it follows that \(T \cup \{t'\} \in {\mathcal {H}}(\varphi )\).
- Case \(T \notin {\mathcal {H}}(\varphi )\), then \(T \cup \{{\tilde{t}}\} \notin {\mathcal {H}}(\varphi )\) for any trace \({\tilde{t}}\). In particular \(T \cup \{t'\} \notin {\mathcal {H}}(\varphi )\).

- Case \(T \notin {\mathcal {H}}(\varphi )\), then \({T \cap {\mathcal {L}}({\mathcal {A}}_\varphi [t/\pi _1]) = \emptyset }\) and \({T \cap {\mathcal {L}}({\mathcal {A}}_\varphi [t/\pi _2]) = \emptyset }\). Therefore also \({T \cap {\mathcal {L}}({\mathcal {A}}_\varphi [t'/\pi _1]) = \emptyset }\) and \({T \cap {\mathcal {L}}({\mathcal {A}}_\varphi [t'/\pi _2]) = \emptyset }\). By Corollary 6, it follows that \(T \cup \{t'\} \notin {\mathcal {H}}(\varphi )\).
- Case \(T \in {\mathcal {H}}(\varphi )\), then \(T \cup \{{\tilde{t}}\} \in {\mathcal {H}}(\varphi )\) for any trace \({\tilde{t}}\). In particular \(T \cup \{t'\} \in {\mathcal {H}}(\varphi )\).

- Case \(T \in {\mathcal {H}}(\varphi )\), then for all \(t_1 \in T\) there is a \(t_2 \in T\) such that \((\emptyset , \{\pi \mapsto t_1, \pi ' \mapsto t_2\}, 0) \vDash \psi \). Especially, for t, there is a corresponding trace \({\tilde{t}}\) such that \((\emptyset , \{\pi \mapsto t, \pi ' \mapsto {\tilde{t}}\}, 0) \vDash \psi \), thus \({\tilde{t}} \in {\mathcal {L}}({\mathcal {A}}_\varphi [t/\pi ])\). From (a) it follows that \({\tilde{t}} \in {\mathcal {L}}({\mathcal {A}}_\varphi [t'/\pi ])\) as well. Hence, \((\emptyset , \{\pi \mapsto t', \pi ' \mapsto {\tilde{t}}\}, 0) \vDash \psi \) and thereby \(T \cup \{t'\} \in {\mathcal {H}}(\varphi )\).
- Case \(T \notin {\mathcal {H}}(\varphi )\), then there exists a \({\tilde{t}} \in T\) such that for all \({\hat{t}} \in T\)\((\emptyset , \{\pi \mapsto {\tilde{t}}, \pi ' \mapsto {\hat{t}}\}, 0) \nvDash \psi \) holds. Especially, for t, \((\emptyset , \{\pi \mapsto {\tilde{t}}, \pi ' \mapsto t\}, 0) \nvDash \psi \), thus \({\tilde{t}} \notin {\mathcal {L}}({\mathcal {A}}_\varphi [t/\pi '])\). From (b) it follows that \({\tilde{t}} \notin {\mathcal {L}}({\mathcal {A}}_\varphi [t'/\pi '])\) as well. Hence, \((\emptyset , \{\pi \mapsto {\tilde{t}}, \pi ' \mapsto t'\}, 0) \nvDash \psi \). As there is no trace \({\hat{t}} \in T \cup \{t'\}\) such that \((\emptyset , \{\pi \mapsto {\tilde{t}}, \pi ' \mapsto {\hat{t}}\}, 0) \vDash \psi \), we can conclude \(T \cup \{t'\} \notin {\mathcal {H}}(\varphi )\). \(\square \)

## 5 Evaluation

Symm | trans | refl | ||
---|---|---|---|---|

ObsDet1 | \(\forall \pi . \forall \pi '.\; \Box (I_{\pi } = I_{\pi '}) \rightarrow \Box (O_{\pi } = O_{\pi '})\) | ✓ | ✗ | ✓ |

ObsDet2 | \(\forall \pi . \forall \pi '.\; (I_{\pi } = I_{\pi '}) \rightarrow \Box (O_{\pi } = O_{\pi '})\) | ✓ | ✗ | ✓ |

ObsDet3 | \(\forall \pi . \forall \pi '. (O_\pi = O_\pi ') {\mathcal {W}}(I_\pi \ne I_\pi ')\) | ✓ | ✗ | ✓ |

QuantNoninf | \(\forall \pi _0 \ldots \forall \pi _{c}.~\lnot ((\bigwedge _i I_{\pi _i} = I_{\pi _0}) \wedge \bigwedge _{i \ne j} O_{\pi _i} \ne O_{\pi _j})\) | ✓ | ✗ | ✓ |

EQ | \(\forall \pi . \forall \pi ' .\Box (a_\pi \leftrightarrow a_{\pi '})\) | ✓ | ✓ | ✓ |

Hamming-2 | \(\forall \pi . \forall \pi '. (\diamondsuit (I_\pi \nleftrightarrow I_{\pi '}) \rightarrow ((O_\pi \leftrightarrow O_{\pi '})\) | ✓ | ✗ | ✓ |

ConfMan | \(\forall \pi \forall \pi ' .\big ((\lnot pc_\pi \wedge pc_{\pi '}) \rightarrow \Circle \Box (s_\pi \rightarrow \Circle v_{\pi '})\big )\)\(\wedge \big ((pc_{\pi } \wedge pc_{\pi '}) \rightarrow \Circle \Box (v_\pi \leftrightarrow v_\pi ')\big )\) | ✗ | ✗ | ✗ |