  Hyperproperties are properties of computational systems that require more
than one trace to evaluate, e.g., many information-flow security and
concurrency requirements. Where a trace property defines a set of traces, a
hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and
HyperCTL* have been proposed to express hyperproperties. However, their
semantics are synchronous in the sense that all traces proceed at the same
speed and are evaluated at the same position. This precludes the use of these
logics to analyze systems whose traces can proceed at different speeds and
allow that different traces take stuttering steps independently. To solve this
problem in this paper, we propose an asynchronous variant of HyperLTL. On the
negative side, we show that the model-checking problem for this variant is
undecidable. On the positive side, we identify a decidable fragment which
covers a rich set of formulas with practical applications. We also propose two
model-checking algorithms that reduce our problem to the HyperLTL
model-checking problem in the synchronous semantics.
