We introduce CPDL+, a family of expressive logics rooted in Propositional Dynamic Logic (PDL). In terms of expressive power, CPDL+ strictly contains PDL extended with intersection and converse (a.k.a. ICPDL) as well as Conjunctive Queries (CQ), Conjunctive Regular Path Queries (CRPQ), or some known extensions thereof (Regular Queries and CQPDL). We investigate the expressive power, characterization of bisimulation, satisfiability, and model checking for CPDL+. We argue that natural subclasses of CPDL+ can be defined in terms of the tree-width of the underlying graphs of the formulas. We show that the class of CPDL+ formulas of tree-width 2 is equivalent to ICPDL, and that it also coincides with CPDL+ formulas of tree-width 1. However, beyond tree-width 2, incrementing the tree-width strictly increases the expressive power. We characterize the expressive power for every class of fixed tree-width formulas in terms of a bisimulation game with pebbles. Based on this characterization, we show that CPDL+ has a tree-like model property. We prove that the satisfiability problem is decidable in 2ExpTime on fixed tree-width formulas, coinciding with the complexity of ICPDL. We also exhibit classes for which satisfiability is reduced to ExpTime. Finally, we establish that the model checking problem for fixed tree-width formulas is in \ptime, contrary to the full class CPDL+.


翻译:我们引入了CPDL+,这是一族有表达力的逻辑,根植于Propositional Dynamic Logic(PDL)。在表达力方面,CPDL+严格包含了通过添加交集和逆运算(即ICPDL)扩展的PDL,以及Conjunctive Queries(CQ)、Conjunctive Regular Path Queries(CRPQ)或一些已知扩展(Regular Queries和CQPDL)。我们研究了CPDL+的表达能力、双模拟的表征、可满足性和模型检验。我们认为,可以根据公式的底层图形的树的宽度来定义CPDL+的自然子类。我们证明了基于树宽度2的CPDL+公式与ICPDL等价,它也与树宽度为1的CPDL+公式相同。但是,在树宽度2之外,树宽度的增加会严格增加表达能力。我们基于夹子双模拟游戏的表征,表征了每个固定树宽度公式的表达能力。基于这种表征,我们证明了CPDL+具有树状模型性质。我们证明了在固定树宽度公式上,可满足性问题在2ExpTime上是可判定的,这与ICPDL的复杂度相符。我们还展示了使可满足性简化为ExpTime的类别。最后,我们证明了固定树宽度公式的模型检验问题在\ptime内,与完整类别的CPDL+相反。

0
下载
关闭预览

相关内容

南大《优化方法 (Optimization Methods》课程,推荐!
专知会员服务
77+阅读 · 2022年4月3日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
图机器学习 2.2-2.4 Properties of Networks, Random Graph
图与推荐
10+阅读 · 2020年3月28日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Seq2seq强化,Pointer Network简介
机器学习算法与Python学习
15+阅读 · 2018年12月8日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
keras系列︱深度学习五款常用的已训练模型
数据挖掘入门与实战
10+阅读 · 2018年3月27日
机器学习线性代数速查
机器学习研究会
19+阅读 · 2018年2月25日
【推荐】用Tensorflow理解LSTM
机器学习研究会
36+阅读 · 2017年9月11日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
Arxiv
0+阅读 · 2023年6月5日
Arxiv
0+阅读 · 2023年6月4日
Arxiv
0+阅读 · 2023年6月2日
VIP会员
相关VIP内容
南大《优化方法 (Optimization Methods》课程,推荐!
专知会员服务
77+阅读 · 2022年4月3日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
相关资讯
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
图机器学习 2.2-2.4 Properties of Networks, Random Graph
图与推荐
10+阅读 · 2020年3月28日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Seq2seq强化,Pointer Network简介
机器学习算法与Python学习
15+阅读 · 2018年12月8日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
keras系列︱深度学习五款常用的已训练模型
数据挖掘入门与实战
10+阅读 · 2018年3月27日
机器学习线性代数速查
机器学习研究会
19+阅读 · 2018年2月25日
【推荐】用Tensorflow理解LSTM
机器学习研究会
36+阅读 · 2017年9月11日
相关基金
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
Top
微信扫码咨询专知VIP会员