  We study satisfiability for HyperLTL with a $\forall^*\exists^*$ quantifier
prefix, known to be highly undecidable in general. HyperLTL can express system
properties that relate multiple traces (so-called hyperproperties), which are
often combined with trace properties that specify functional behavior on single
traces. Following this conceptual split, we first define several safety and
liveness fragments of $\forall^*\exists^*$ HyperLTL, and characterize the
complexity of their (often much easier) satisfiability problem. We then add LTL
trace properties as functional specifications. Though (highly) undecidable in
many cases, this way of combining "simple" HyperLTL and arbitrary LTL also
leads to interesting new decidable fragments. This systematic study of
$\forall^*\exists^*$ fragments is complemented by a new (incomplete) algorithm
for $\forall\exists^*$-HyperLTL satisfiability.
