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.

翻译：针对信息流属性规范的时间逻辑能够表达系统多个执行轨迹之间的关系。其中最重要的两种逻辑是HyperLTL和HyperCTL*，它们通过路径量化将LTL和CTL*进行泛化。已知这种表达能力以可判定性为代价——即两种逻辑的可满足性均不可判定。本文确定了这些问题的精确复杂度，证明两者实际上都是高度不可判定的：我们证明了HyperLTL可满足性为$\Sigma_1^1$-完全，而HyperCTL*可满足性为$\Sigma_2^1$-完全。这相较于此前已知的下界有显著提升，并首次给出了上界。为证明HyperCTL*的$\Sigma_1^2$成员性质，我们证明了每个可满足的HyperCTL*公式都存在一个与连续统等势的模型——这是此类问题的首个上界，同时证明了该界是紧的。此外，我们还证明了HyperCTL*的可数可满足性和有限分支可满足性均与二阶算术的真值判定具有相同难度，即仍属高度不可判定。最后，我们证明HyperLTL量词交替层级中每一层的成员性质问题均为$\Pi_1^1$-完全。