| 时序逻辑理论研究：表达能力和复杂性 |
| 其他题名 | On the Theoretical Aspects of Temporal Logics: Expressive Power and Complexity
|
| 吴志林
|
| 2007-06-03
|
| 学位授予单位 | 中国科学院软件研究所
|
| 学位 | 博士
|
| 学位授予地点 | 软件研究所
|
| 关键词 | 时序逻辑
表达能力
复杂性
|
| 摘要 | 本论文主要集中于时序逻辑的理论方面，即表达能力和复杂性。
首先我们将带有循环计数的线性时序逻辑(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)分别与可满足性问题和模型检测问题具有相同的复杂度。 |
| 其他摘要 | In this thesis, we focus on the theoretical aspects, namely expressive power and complexity, of propositional temporal logics.
First we extend the effective characterization of linear temporal logic with cyclic counting(LTL[C]) from finite words to infinite words, we define the omega-quasi-star-free languages (QSF^I) and show that LTL[C] expresses exactly QSF^I.
Then we investigate systematically the expressive power of QLTL: we show that the single ``U'(Until) or ``F'(Future) temporal operator suffices to express the whole class of (omega-)regular languages with the help of quantifiers (the resulting fragments of QLTL are denoted by Q(U) and Q(F), resp.); and we compare the expressive power of various fragments of QLTL in detail; moreover we study the quantifier hierarchy of Q(U) and Q(F) and prove that one alternation of existential and universal quantifiers is necessary and sufficient for Q(U) and Q(F) to express the whole class of (omega-)regular languages; we also discuss the similar problems for the strict ``Until' and ``Future' temporal operators.
Then, following the Ehrenfeucht-Fraisse Game approach, we we simplify the proof of the characterization of TL[EFs] given by Bojanczyk&Walukiewicz, and extend the proof to the characterization of TL[EF].,
We finally consider dual models problem of LTL in analogy with the NAESAT problem of Boolean logic, and proved that dual models problem (DM) and the problem of determination of dual models in a Kripke structure (KDM) have the same complexity with satisfiability and model checking problem respectively. |
| 页数 | 118
|
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/5932
|
| 专题 | 中科院软件所_中科院软件所
|
推荐引用方式
GB/T 7714 |
吴志林. 时序逻辑理论研究：表达能力和复杂性[D]. 软件研究所. 中国科学院软件研究所,2007.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论