CISPA
Browse
BFFM23.pdf (809.8 kB)

Second-Order Hyperproperties

Download (809.8 kB)
We introduce Hyper2LTL, 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, Hyper2LTL can express complex epistemic properties like common knowledge, Mazurkiewicz trace theory, and asynchronous hyperproperties. The model checking problem of Hyper2LTL 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.

History

Editor

Enea C ; Lal A

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification (CAV)

Journal

CAV (2)

Volume

13965

Page Range

309-332

Publisher

Springer Nature

Open Access Type

  • Hybrid

BibTeX

@inproceedings{Beutner:Finkbeiner:Frenkel:Metzger:2023, title = "Second-Order Hyperproperties", author = "Beutner, Raven" AND "Finkbeiner, Bernd" AND "Frenkel, Hadar" AND "Metzger, Niklas", editor = "Enea, Constantin" AND "Lal, Akash", year = 2023, month = 7, journal = "CAV (2)", pages = "309--332", publisher = "Springer Nature", issn = "1611-3349", doi = "10.1007/978-3-031-37703-7_15" }