时序逻辑理论研究：表达能力和复杂性
文献类型：学位论文
| 作者 | 吴志林 |
| 学位类别 | 博士 |
| 答辩日期 | 2007-06-03 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 软件研究所 |
| 关键词 | 时序逻辑 表达能力 复杂性 |
| 其他题名 | On the Theoretical Aspects of Temporal Logics: Expressive Power and Complexity |
| 中文摘要 | 本论文主要集中于时序逻辑的理论方面，即表达能力和复杂性。 首先我们将带有循环计数的线性时序逻辑(LTL[C])的有限字上的刻画扩展到无限字上：我们定义了omega-半无星语言（omega-quasi-star-free languages，简记为QSF^I），然后证明了LTL[C]刚好表达了QSF^I。 接着我们系统地探讨了QLTL的表达能力：我们证明了在量词的帮助下单个的“U”（“Until”）或者“F”（“Future”）时态算子就可以表达整个的(omega-)正规语言（QLTL对应的子集分别记为Q(U)和Q(F)）；然后我们对QLTL的各个子集的表达能力进行了详细的比较；而且我们讨论了Q(U)和Q(F)中的量词层次，我们证明了存在量词和全称量词只需要嵌套一次就能表达整个(omega-)正规语言类；我们也对严格的“Until”和“Future”算子讨论了类似的问题。 然后我们用Ehrenfeucht-Fraisse博弈对Bojanczyk&Walukiewicz关于TL[EFs]的刻画进行了简化并且将其推广到对TL[EF]的刻画上。 最后，我们类比于布尔逻辑的NAESAT问题考虑了LTL的对偶模型问题：我们证明了对偶模型问题(DM)和在一个Kripke结构中判定对偶模型的问题(KDM)分别与可满足性问题和模型检测问题具有相同的复杂度。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 118 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/5932]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 吴志林. 时序逻辑理论研究：表达能力和复杂性[D]. 软件研究所. 中国科学院软件研究所. 2007. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。