一句话：提出 HyperLTL 的两种异步正交扩展 HyperLTLS 与 HyperLTLC，证明一般模型检测不可判定并给出可判定片段及复杂度。
HyperLTL 等超属性时序逻辑通常采用同步语义，难以直接表达异步信息流安全等需求。本文引入两种异步且正交的扩展：Stuttering HyperLTL（HyperLTLS）与 Context HyperLTL（HyperLTLC）。作者证明这两个逻辑的模型检测问题一般是不可判定的，同时分别识别出一个可判定的模型检测片段；这些片段均包含 HyperLTL，并能表达有意义的异步要求。文章进一步给出这两个片段模型检测的精确计算复杂度，其中 HyperLTLS 片段的复杂度与表达力更弱的 HyperLTL 相同。
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.