We settle the complexity of satisfiability, finite-state satisfiability, and model-checking for generalized HyperLTL with stuttering and contexts, an expressive logic for the specification of asynchronous hyperproperties. Such properties cannot be specified in HyperLTL, as it is restricted to synchronous hyperproperties. Nevertheless, we prove that satisfiability is $Σ_1^1$-complete and thus not harder than for HyperLTL. On the other hand, we prove that model-checking and finite-state satisfiability are equivalent to truth in second-order arithmetic, and thus much harder than the decidable HyperLTL model-checking problem and the $Σ_0^1$-complete HyperLTL finite-state satisfiability problem. The lower bounds for the model-checking and finite-state satisfiability problems hold even when only allowing stuttering or only allowing contexts.

翻译：我们确定了带停顿与语境的广义HyperLTL逻辑（一种用于异步超性质规约的表达性逻辑）的可满足性、有穷状态可满足性及模型检验问题的计算复杂度。此类超性质无法在局限于同步超性质的HyperLTL中规约。尽管如此，我们证明其可满足性问题是$Σ_1^1$完备的，因此并不比HyperLTL更困难。另一方面，我们证明模型检验与有穷状态可满足性问题等价于二阶算术真值问题，因而远难于可判定的HyperLTL模型检验问题及$Σ_0^1$完备的HyperLTL有穷状态可满足性问题。即使在仅允许停顿或仅允许语境的限制条件下，模型检验与有穷状态可满足性问题的下界仍然成立。