Institutional Repository
| 时序逻辑理论研究：表达能力和复杂性 | |
| Alternative Title | On the Theoretical Aspects of Temporal Logics: Expressive Power and Complexity |
| 吴志林 | |
| 2007-06-03 | |
| Degree Grantor | 中国科学院软件研究所 |
| Degree Level | 博士 |
| Place of Degree Grantor | 软件研究所 |
| Keyword | 时序逻辑 表达能力 复杂性 |
| English Abstract | 本论文主要集中于时序逻辑的理论方面，即表达能力和复杂性。 首先我们将带有循环计数的线性时序逻辑(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)分别与可满足性问题和模型检测问题具有相同的复杂度。 |
| Abstract | 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. |
| Pages | 118 |
| Language | 中文 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/5932 |
| Collection | 中科院软件所_中科院软件所 |
| Recommended Citation GB/T 7714 | 吴志林. 时序逻辑理论研究：表达能力和复杂性[D]. 软件研究所. 中国科学院软件研究所,2007. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 10001_20041801502902（1265KB） | 限制开放 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment