Hyperproperties are a modern specification paradigm that extends properties of a single trace to express properties of a set 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, Stuttering HyperLTL (HyperLTL S ) and Context HyperLTL (HyperLTL C ). 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 problem 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 (HyperLTL S ) fragment, coincides with that of the strictly less expressive logic HyperLTL.
Bozzelli et al. (Tue,) studied this question.