中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
时序逻辑理论研究:表达能力和复杂性
作者: 吴志林
答辩日期: 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)分别与可满足性问题和模型检测问题具有相同的复杂度。
英文摘要: 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.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/5932
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200418015029020吴志林_paper.pdf(1265KB)----限制开放-- 联系获取全文

Recommended Citation:
吴志林. 时序逻辑理论研究:表达能力和复杂性[D]. 软件研究所. 中国科学院软件研究所. 2007-06-03.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[吴志林]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[吴志林]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace