We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is $Σ_1^2$-complete, and finite-state satisfiability and model-checking are equivalent to truth in second-order arithmetic. Finally, we also introduce closed-world semantics for second-order HyperLTL, where set quantification ranges only over subsets of the model, while set quantification in standard semantics ranges over arbitrary sets of traces. Here, satisfiability for the least fixed point fragment becomes $Σ_1^1$-complete, but all other results are unaffected.

翻译：我们确定了二阶HyperLTL的可满足性、有限状态可满足性和模型检测的复杂性：这三者均等价于三阶算术的真值判定问题。我们还考察了二阶HyperLTL的两个片段，这些片段通过限制可量化的集合范围来促进有效模型检测。第一个片段将二阶量化限制为满足守卫条件的最小/最大集合，第二个片段则进一步将二阶量化限制为（一阶）HyperLTL可定义函数的最小不动点。对于第一个片段，所有三个问题仍等价于三阶算术的真值判定；而对于第二个片段，其可满足性问题是$Σ_1^2$完全的，有限状态可满足性与模型检测则等价于二阶算术的真值判定。最后，我们为二阶HyperLTL引入了封闭世界语义，其中集合量化仅限定在模型的子集范围内，而标准语义中的集合量化则涵盖任意迹集合。在此语义下，最小不动点片段的可满足性问题变为$Σ_1^1$完全的，但所有其他结果保持不变。