中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
学科主题: 计算机软件::软件理论
题名:
关于可满足性问题的一些研究及其在模型检测中的应用
作者: 陈伟
答辩日期: 2010-05-31
导师: 张文辉
授予单位: 中国科学院研究生院
授予地点: 北京
学位: 博士
关键词: 命题逻辑证明系统,OBDD证明系统,鸽笼问题,限界模型检测,CTL
摘要: 命题逻辑证明复杂性的研究自从70年代初期由Cook等人提出开始,就一直迅速发展。 Cook等人提出这一领域的初衷是通过证明NP<>CoNP来证明P<>NP。 这一领域近年来的研究内容包括如下几个方向:第一个方向就是“指数下界”问题:也就是证明对于某一个特定的命题逻辑证明系统,存在一个自然的不可满足的公式实例,该系统对这个实例最短的证明规模都是关于实例长度指数级别的; 第二个方向就是比较不同命题逻辑证明系统之间的能力强弱。另一方面,模型检验技术自从80年代由Clarke等人提出用以自动化的检验软硬件系统性质正确性以来,同样的发展迅速。贯穿模型检验技术发展的一个主线就是试图解决系统状态数目过多无法完全在计算机中存储表示的问题,这个问题我们一般称为“状态爆炸”。为了缓解状态爆炸问题,1999年Biere等人提出把命题逻辑可满足性求解工具应用在模型检测领域的限界模型检测方法,相比传统的模型检验算法,对于部分性质,可以极大的减少需要表示的系统状态空间数目,缓解状态爆炸问题。 本文主要包含两部分的内容:第一部分的内容是关于OBDD证明系统的一个理论结果和实际求解的一个解法器的描述。概括的讲,我们解决了Atserias等人在CP2004会议上提出的关于OBDD证明系统的一个问题:我们给出了针对鸽笼问题的多项式规模的OBDD证明系统的一个直接构造,并严格证明了该构造的多项式规模;并且在这个理论结果的基础之上,我们设计了基于OBDD证明系统的实际的求解器,这个求解器可以在多项式时间内解决鸽笼和其他与鸽笼问题结构上相似的实例,这是其他的已知的基于OBDD的求解器无法做到的。这部分内容可以看做是命题逻辑证明复杂性里面第二个方向下的内容,在这里,我们把鸽笼问题 作为一个标尺问题,可以把OBDD证明系统的能力同其他对鸽笼问题的证明为指数的命题逻辑证明系统区分开来。 第二部分的内容是关于限界模型检测的。限界模型检测,是利用命题逻辑可满足性问题求解器来解决一般模型检测问题的方法。对于原本用来描述系统时序性质的时序逻辑的算子,该方法用命题逻辑公式表达出来(在系统迁移关系步数受限的情况下),这个过程就是编码。编码之后,再使用命题逻辑可满足性求解工具来求解。在这部分工作中,我们关注的逻辑是CTL逻辑的fragments,即ECTL或者ACTL,我们详细研究了并改进了ECTL和ACTL到命题逻辑的编码,并且把这个编码过程实现到了开源的模型检测工具平台NuSMV 2上,通过实验来对比限界模型检测方法的效率。实验结果表明,对于某些性质来说,我们的方法相比于传统的基于OBDD的模型检测算法具有优势。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/2304
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
200618015029026软件所——陈伟.pdf(842KB)----限制开放 联系获取全文

Recommended Citation:
陈伟. 关于可满足性问题的一些研究及其在模型检测中的应用[D]. 北京. 中国科学院研究生院. 2010-05-31.
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