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_1^2 $-完全的。 这些都是先前已知下限的显着增加以及第一个上限。为了证明超时态CTL *的$ \Sigma_1^2 $-成员资格，我们证明每个可满足的HyperCTL *句子都有一个模型，它与连续体具有相同数量，这是这种类型的第一个上限。我们还证明这个上限是严格的。此外，我们证明超时态CTL *的可数和有限分支可满足性都像二阶算术中的真实性那样难，即仍然非常不可判定。最后，我们表明，HyperLTL量词交替层次的每个级别的成员资格问题都是$ \Pi_1^1 $-完全的。