一句话：确定 HyperLTL 与 HyperCTL* 可满足性的精确复杂度：分别为 Σ₁¹-完备与 Σ₁²-完备。
HyperLTL 和 HyperCTL* 通过迹量化扩展 LTL 与 CTL*，可描述多执行间关系及信息流性质，但其可满足性此前仅知不可判定。本文精确刻画其复杂度：HyperLTL 可满足性是 Σ₁¹-完备的，HyperCTL* 可满足性是 Σ₁²-完备的，显著提高了已知下界并首次给出上界。为证明 HyperCTL* 的 Σ₁² 成员性，作者证明每个可满足的 HyperCTL* 语句都有一个与连续统等势的模型，并证明该界是紧的。此外，HyperCTL* 的可数可满足性与有限分支可满足性仍与二阶算术真值同难；HyperLTL 量词交替层级的成员问题均为 Π₁¹-完备。
Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics. In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is $\Sigma_1^1$-complete and HyperCTL* satisfiability is $\Sigma_1^2$-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove $\Sigma_1^2$-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We also prove this bound to be tight. Furthermore, we prove that both countable and finitely-branching satisfiability for HyperCTL* are as hard as truth in second-order arithmetic, i.e. still highly undecidable. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is $\Pi_1^1$-complete.Comment: arXiv admin note: substantial text overlap with arXiv:2105.04176
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FortinKTZ25,
title = {HyperLTL Satisfiability Is Highly Undecidable, HyperCTL$^*$ is Even Harder},
author = {Marie Fortin and Louwe B. Kuijer and Patrick Totzke and Martin Zimmermann},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:3)2025}
}