We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are as hard as 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. The first fragment is still as hard as truth in third-order arithmetic while satisfiability for the second one is $\Sigma_1^1$-complete, i.e., only as hard as (first-order) HyperLTL and therefore much less complex. Finally, finite-state satisfiability and model-checking are in $\Sigma_2^2$ and $\Sigma_1^1$-hard, and thus also less complex than model-checking full second-order HyperLTL.

翻译：我们确定了二阶HyperLTL的可满足性、有限状态可满足性和模型检测的复杂度：三者均与三阶算术中的真值判定问题同难度。我们还考察了二阶HyperLTL的两个子片段，这些片段旨在通过限制可量化的集合范围来促进有效的模型检测。第一个片段将二阶量化限制为满足保护条件的最小/最大集合，第二个片段则进一步将二阶量化限制为（一阶）HyperLTL可定义函数的最小不动点。第一个片段的复杂度仍与三阶算术真值判定相当，而第二个片段的可满足性为$\Sigma_1^1$-完全阶，即仅与（一阶）HyperLTL同难度，因此复杂度大幅降低。最后，有限状态可满足性和模型检测属于$\Sigma_2^2$且为$\Sigma_1^1$-困难，因此其复杂度也低于完整二阶HyperLTL的模型检测。