Logics for the specification of hyperproperties

Since the 1980s, model checking has become a staple in verification. For Linear Temporal Logic (LTL) and its progeny, the model checking problem asks whether every trace of a given system fulfils a given temporal specification such as a liveness or fairness property. Notably, this specification considers the traces of the input in isolation and cannot relate different traces to each other. However, it is not hard to come up with natural properties that require viewing different traces in tandem. A textbook example is bounded termination; one cannot decide whether a system terminates in bounded time by considering computation traces of the system in isolation. Further typical properties of this kind are many information-flow properties of systems such as observational determinism or generalised non-interference. A common term coined for properties of the aforementioned kind are hyperproperties (in contrast to trace properties). Hyperproperties describe properties of sets of traces, and since LTL and other traditional temporal logics can only specify trace properties, new logics have needed to be designed to fill this gap. In this talk, I review two approaches for designing logics for hyperproperties: a) HyperLTL and is progeny that are obtained from classical temporal logics by extending their syntax with quantifiers ranging over traces, b) TeamLTL and its variants, which adopt team semantics and lift the satisfaction of LTL formulae to sets of traces directly. In addition to introducing these logical formalism, I will review their expressive power (in relation to each other) and the complexity of their model checking and satisfiability problems.