  Hyperproperties are a modern specification paradigm that extends trace
properties to express properties of sets of traces. Temporal logics for
hyperproperties studied in the literature, including HyperLTL, assume a
synchronous semantics and enjoy a decidable model checking problem. In this
paper, we introduce two asynchronous and orthogonal extensions of HyperLTL,
namely Stuttering HyperLTL (HyperLTLS) and Context HyperLTL (HyperLTLC). Both
of these extensions are useful, for instance, to formulate asynchronous
variants of information-flow security properties. We show that for these
logics, model checking is in general undecidable. On the positive side, for
each of them, we identify a fragment with a decidable model checking that
subsumes HyperLTL and that can express meaningful asynchronous requirements.
Moreover, we provide the exact computational complexity of model checking for
these two fragments which, for the HyperLTLS fragment, coincides with that of
the strictly less expressive logic HyperLTL.
