HyperLTL¶
We consider hyperproperties as formulas in HyperLTL [1], which allows explicit quantification on traces. The syntax of HyperLTL formulas is defined by the following grammar:
\[\begin{split}\begin{array}{rcl}
\varphi & ::= & \exists \pi . \varphi \mid \forall \pi . \varphi \mid \phi \\
\phi & ::= & \mathit{true} \mid a_\pi \mid \neg \phi \mid \phi \lor \phi \mid \phi \land \phi \mid \phi \mathcal{U} \phi \mid \phi \mathcal{R} \phi \mid \bigcirc \phi
\end{array}\end{split}\]
References¶
Temporal logics for hyperproperties. In Proceedings of the 3rd Conference on Principles of Security and Trust POST, pages 265–284, 2014. M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. Sánchez