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中指定，因为HyperLTL仅限于同步超性质。尽管如此，我们证明了可满足性是$Σ_1^1$-完全的，因此并不比HyperLTL更困难。另一方面，我们证明了模型检测和有限状态可满足性等价于二阶算术中的真值，因此比可判定的HyperLTL模型检测问题和$Σ_0^1$-完全的HyperLTL有限状态可满足性问题困难得多。模型检测和有限状态可满足性问题的下界即使在仅允许停滞或仅允许上下文的情况下仍然成立。