Second-Order Hyperproperties
Abstract
We introduce HyperLTL, a temporal logic for the specification of hyperproperties that allows for second-order quantification over sets of traces. Unlike first-order temporal logics for hyperproperties, such as HyperLTL, HyperLTL can express complex epistemic properties like common knowledge, Mazurkiewicz trace theory, and asynchronous hyperproperties. The model checking problem of HyperLTL is, in general, undecidable. For the expressive fragment where second-order quantification is restricted to smallest and largest sets, we present an approximate model-checking algorithm that computes increasingly precise under- and overapproximations of the quantified sets, based on fixpoint iteration and automata learning. We report on encouraging experimental results with our model-checking algorithm, which we implemented in the tool~\texttt{HySO}.
Cite
@article{arxiv.2305.17935,
title = {Second-Order Hyperproperties},
author = {Raven Beutner and Bernd Finkbeiner and Hadar Frenkel and Niklas Metzger},
journal= {arXiv preprint arXiv:2305.17935},
year = {2023}
}