HyperLTL可满足性是高度不可判定的，HyperCTL$^*$的难度更高
HyperLTL Satisfiability Is Highly Undecidable, HyperCTL$^*$ is Even Harder
AI总结：
该研究确定了HyperLTL与HyperCTL*两种信息流时序逻辑可满足性问题的精确不可判定复杂度，给出了对应复杂度类的上下界，并证明了相关衍生问题的难度等级。
摘要：
用于规约信息流属性的时序逻辑能够表达系统多次执行之间的关系。这类逻辑中最重要的两种是HyperLTL和HyperCTL*，它们通过迹量化推广了LTL和CTL*。已知这种表达能力是有代价的，即两种逻辑的可满足性都是不可判定的。本文确定了这些问题的确切复杂度，证明二者实际上都是高度不可判定的：我们证明HyperLTL可满足性是$Σ_1^1$-完全的，HyperCTL*可满足性是$Σ_1^2$-完全的。相比此前已知的下界，这些结果显著提升了复杂度等级，同时也是首个上界。为证明HyperCTL*属于$Σ_1^2$，我们证明每个可满足的HyperCTL*语句都存在一个与连续统等势的模型，这是该类问题的首个上界，且我们证明该界是紧的。此外，我们证明HyperCTL*的可数可满足性和有穷分支可满足性都与二阶算术真值判定问题难度相当，即仍为高度不可判定。最后，我们表明HyperLTL量词交替分层每一层的成员问题都是$Π_1^1$-完全的。
英文摘要：
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 $Σ_1^1$-complete and HyperCTL* satisfiability is $Σ_1^2$-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove $Σ_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 $Π_1^1$-complete.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
