一句话：确定了二阶 HyperLTL 可满足性、有限状态可满足性与模型检测的复杂度，并分析两个受限片段及闭世界语义。
本文研究二阶 HyperLTL 的可满足性、有限状态可满足性与模型检测复杂度，其二阶量词可作用于迹集合。作者证明三者均等价于三阶算术真值。为便于有效模型检测，论文考察两个受限片段：其一将二阶量化限制为满足守卫的最大/最小集合，三个问题仍等价于三阶算术真值；其二限制为一阶 HyperLTL 可定义函数的最小不动点，此时可满足性为 Σ_1^2 完全，有限状态可满足性与模型检测等价于二阶算术真值。最后引入闭世界语义，将集合量化限制在模型子集上；该语义下最小不动点片段可满足性变为 Σ_1^1 完全，其余结果不变。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FrenkelRZ26,
title = {The Complexity of Second-order HyperLTL},
author = {Hadar Frenkel and Gaëtan Regaud and Martin Zimmermann},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 1},
year = {2026},
doi = {10.46298/lmcs-22(1:26)2026}
}