Temporal Logics for Hyperproperties

Abstract. Two new logics for verification of hyperproperties are pro-posed. Hyperproperties characterize security policies, such as noninter-ference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL ∗ can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL∗, add explicit and simultane-ous quantification over multiple paths to LTL and to CTL∗. This kind of quantification enables expression of hyperproperties. A model checking algorithm for a fragment of HyperLTL is given. The algorithm has been implemented in a prototype model checker.