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 $-完全的。

0
下载
关闭预览

相关内容

【硬核书】矩阵代数基础,248页pdf
专知会员服务
84+阅读 · 2021年12月9日
专知会员服务
32+阅读 · 2021年10月9日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
58+阅读 · 2019年10月17日
论文浅尝 | Neural-Symbolic Models for Logical Queries on KG
开放知识图谱
0+阅读 · 2022年10月31日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
征稿 | International Joint Conference on Knowledge Graphs (IJCKG)
开放知识图谱
2+阅读 · 2022年5月20日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【SIGIR2018】五篇对抗训练文章
专知
12+阅读 · 2018年7月9日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
Arxiv
0+阅读 · 2023年5月17日
VIP会员
相关资讯
论文浅尝 | Neural-Symbolic Models for Logical Queries on KG
开放知识图谱
0+阅读 · 2022年10月31日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
征稿 | International Joint Conference on Knowledge Graphs (IJCKG)
开放知识图谱
2+阅读 · 2022年5月20日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【SIGIR2018】五篇对抗训练文章
专知
12+阅读 · 2018年7月9日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
Top
微信扫码咨询专知VIP会员