Temporal Hyperproperties
Bernd Finkbeiner
Hyperproperties generalize trace properties, which are sets of traces, to sets of sets of traces. The most prominent application of hyperproperties is information flow security: information flow policies characterize the secrecy and integrity of a system by comparing two or more execution traces, for example by comparing the outputs on execution traces that result from different values of a secret input. HyperLTL is an extension of linear-time temporal logic (LTL) with explicit quantification over traces. In this overview paper, we survey recent results on the expressiveness of HyperLTL and on the satisfiability and model checking problems. We also consider HyperCTL*, the extension of HyperLTL to branching time, and HyperFOLTL, the extension of HyperLTL with first-order quantification.
The Logic in Computer Science Column by Yuri Gurevich (Bulletin of EATCS).