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.
翻译:信息流属性规约的时间逻辑能够表达系统多个执行之间的关系。其中,最常用的两种逻辑是通过跟踪量化推广的LTL和CTL*的HyperLTL和HyperCTL*。已知这种表现力是有代价的,即对于这两种逻辑,可满足性问题是不可判定的。在本文中,我们解决了这些问题的确切复杂性,证明了它们都是高度不可判定的:我们证明了HyperLTL可满足性是$\Sigma_1^1$-完全的,HyperCTL*可满足性是$\Sigma_1^2$-完全的。这些是之前已知下界的显著增长,也是首个上界。为了证明HyperCTL*的$\Sigma_1^2$-成员资格,我们证明了所有可满足HyperCTL*句子都有一个与连续体数量相等的模型,这是这种上界的首次。我们还证明这个上界是紧的。此外,我们证明,HyperCTL*的所有可数和有限分支可满足性都与二阶算术的真相一样难,即仍然高度不可判定。最后,我们展示了HyperLTL量词交替层次的成员资格问题是$\Pi_1^1$-完全的。