Second-Order Hyperproperties

TL;DR

This paper introduces Hyper$^2$LTL, a second-order temporal logic for hyperproperties, enabling the expression of complex properties like common knowledge and asynchronous hyperproperties, with an approximate model-checking algorithm for a specific fragment.

Contribution

The paper presents Hyper$^2$LTL, a novel second-order logic for hyperproperties, and an approximate model-checking algorithm for a restricted expressive fragment.

Findings

Implemented in the tool HySO

Encouraging experimental results

Approximate model checking for a specific fragment

Abstract

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