• Hyper properties are sets of sets of traces where properties are sets of traces
  • For example we want a system where lights are on at the same time (Hyper LTL)
    • $\forall x_1{x}_2,P(x_1)\leftrightarrow P(x_2)$
    • satisfiability is undecidable
  • Asynch extension for Hyperltl with Fixpoint operator and alternating automata
    • model checking is decidable, so we look at a decidable fragment.
    • How to compare different extensions
  • Context HyperLTL
    • which has teh extra temporal operator $⟨C⟩\psi$ where $\varphi$ is a temporal formula and the operator says only extend the traces in $C$