  HyperLTL is an extension of linear-time temporal logic for the specification
of hyperproperties, i.e., temporal properties that relate multiple computation
traces. HyperLTL can express information flow policies as well as properties
like symmetry in mutual exclusion algorithms or Hamming distances in
error-resistant transmission protocols. Previous work on HyperLTL model
checking has focussed on the alternation-free fragment of HyperLTL, where
verification reduces to checking a standard trace property over an appropriate
self-composition of the system. The alternation-free fragment does, however,
not cover general hyperliveness properties. Universal formulas, for example,
cannot express the secrecy requirement that for every possible value of a
secret variable there exists a computation where the value is different while
the observations made by the external observer are the same. In this paper, we
study the more difficult case of hyperliveness properties expressed as HyperLTL
formulas with quantifier alternation. We reduce existential quantification to
strategic choice and show that synthesis algorithms can be used to eliminate
the existential quantifiers automatically. We furthermore show that this
approach can be extended to reactive system synthesis, i.e., to automatically
construct a reactive system that is guaranteed to satisfy a given HyperLTL
formula.
