| Title: | 分布式系统中必然方式下的谓词检测 |
| Author: | 黄洪涛
|
| Issued Date: | 2009-06-04
|
| Supervisor: | 张文辉
|
| Degree Grantor: | 中国科学院软件研究所
|
| Place of Degree Grantor: | 中国科学院软件研究所5号楼337
|
| Degree Level: | 硕士
|
| Abstract: | 本文研究了Definitely模态下分布式计算的谓词检测问题，即判断在计算产生的格状态空间中，是否每条从最小元到最大元的路径都通过一个满足谓词的状态。本文的主要内容有以下四个方面：
１、本文建立了一个逻辑公式用来描述一个DNF谓词在Definitely模态下的检测是否为真。这个逻辑公式给出了一个新的方式用以考察对于DNF谓词Definitely模态的含义。由这个逻辑公式可以导出一种原有的区间缩减技术：区间压缩。接下来使用这个逻辑公式，还可以得到两种新的区间缩减技术：区间组合和区间删除。为了进行区间组合和区间删除，本文将计算表示成Hasse图，同时给出了一个化简Hasse图的方法。
２、本文给出了两类DNF谓词，它们可以按照与合取谓词类似的方式检测，因此有多项式时间的检测算法。这两类DNF谓词是：分离DNF谓词和分离-包含DNF谓词。
３、必然状态和必然集合在上面两类DNF谓词的检测中起着重要作用，因此本文研究了必然状态和必然集合的一些性质。接下来本文提出了区域独立的概念，区域独立是上面两类DNF谓词有多项式时间检测算法的本质，同时给出了区域独立的一些基本性质。
４、本文证明了正则谓词在Definitely模态下的检测是coNP完全的，回答了文献中提出的未解决的问题。接下来研究了一种特殊情况下正则谓词在Definitely模态下的检测。这种特殊情况是：计算的所有状态都是一致的，称这时的状态空间为全空间。本文给出了全空间情况下对于正则谓词，Definitely模态和Invariant模态之间的关系。并且给出了一种算法，它在全空间情况下通过测试n条简单路进行Definitely模态下正则谓词的检测，其时间复杂度是O(n|E|)，其中n为计算中进程的个数，|E|是计算中所有事件的个数。 |
| Language: | 中文
|
| Content Type: | 学位论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/113
|
| Appears in Collections: | 计算机科学国家重点实验室 _学位论文
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| Thesis.pdf（1741KB） | -- | -- | 限制开放 | | 联系获取全文 |
|
| Recommended Citation: | |
黄洪涛. 分布式系统中必然方式下的谓词检测[D]. 中国科学院软件研究所5号楼337. 中国科学院软件研究所. 2009-06-04.
|
|
|
