| 题名 | 关于可满足性问题的一些研究及其在模型检测中的应用 |
| 作者 | 陈伟 |
| 学位类别 | 博士 |
| 答辩日期 | 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的模型检测算法具有优势。 |
| 语种 | 中文 |
| 学科主题 | 软件理论 |
| 公开日期 | 2010-06-04 |
| 内容类型 | 学位论文 |
| 源URL | [http://124.16.136.157/handle/311060/2304]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _学位论文 |
| 推荐引用方式 GB/T 7714 | 陈伟. 关于可满足性问题的一些研究及其在模型检测中的应用[D]. 北京. 中国科学院研究生院. 2010. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论