Second-Order Hyperproperties

(2023) Second-Order Hyperproperties.

Text BFFM23.pdf Download (829kB)

Abstract

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.

Item Type:	Conference or Workshop Item (A Paper) (Paper)
Divisions:	Bernd Finkbeiner (Reactive Systems Group, RSG)
Conference:	CAV Computer Aided Verification
Depositing User:	Hadar Frenkel
Date Deposited:	29 Aug 2023 05:38
Last Modified:	29 Aug 2023 05:38
Primary Research Area:	NRA2: Reliable Security Guarantees
URI:	https://publications.cispa.saarland/id/eprint/3981

Actions

Actions (login required)

View Item