分布式系统中必然方式下的谓词检测

本文研究了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|是计算中所有事件的个数。