Second-Order Hyperproperties

Beutner, Raven and Finkbeiner, Bernd and Frenkel, Hadar and Metzger, Niklas
(2023) Second-Order Hyperproperties.
In: CAV 2023, 17-22/07/23, Paris.
Conference: CAV Computer Aided Verification

[img] Text

Download (829kB)


We introduce Hyper^2LTL, 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, Hyper^2LTL can express complex epistemic properties like common knowledge, Mazurkiewicz trace theory, and asynchronous hyperproperties. The model checking problem of Hyper^2LTL 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 HySO.


Actions (login required)

View Item View Item