分布式CTL模型检测的基本定义和算法

《理论计算机科学电子札记》68卷第4期（2002年）网址：http://www.elsevier.nl/locate/entcs/volume68.html16页使用假设分布CTL模型检测LubosBrima，1，2，Jitk aCrhova′a，1，3，KarenYoravb，4a捷克共和国b以色列海法理工学院和美国摘要在这项工作中，我们讨论的问题进行分布式CTL模型检测分裂成几个“部分状态空间”的给定的状态空间。 部分状态空间被建模为边界状态的Kripke结构。参与分布式计算的每台计算机都拥有一个部分状态空间，并执行一个模型检测算法在这个不完整的结构。 为了能够继续进行，边界状态被关于公式的真实性的假设所增强，并且计算机在计算更精确的信息时交换关于相关状态的假设。本文给出了其基本定义，并给出了分布式算法。1介绍开发分布式模型检测环境的主要目的是将模型检测算法的适用性扩展到更大、更复杂的系统。已经提出了许多“顺序”方法来处理大的状态空间，例如偏序方法，符号验证，抽象和部分状态空间推理。通常这些方法并不适用于- 时间或空间资源仍然会显著地限制实际应用。并行超级计算机、网格或计算机网络可以提供解决更现实的验证问题所需的额外资源。在这里，我们考虑一个廉价的变体1由捷克共和国资助机构资助的研究201/00/1023和由教育部通过FRVSNo.B598/G4/20022电子邮件地址：brim@fi.muni.cz3电子邮件地址：xcrhova@fi.muni.cz4电子邮件地址：laster@cs.technion.co.il2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。BRIM、CRHOVA′和Y或AV2在分布式环境中运行的算法的重要特征是通过在参与的工作站之间以尽可能小的协调量分配数据来解决给定的任务。分布式模型检测算法的主要问题之一是如何在这里称为网络节点的各个计算机之间划分状态空间（数据）。在分布式环境中，有两个方面显著地影响模型检查的整体效率：状态空间划分的局部性和（空间）平衡。局部性意味着大多数状态的派生变量被分配给与父状态相同的节点，从而减少了通信和协作开销。平衡意味着每个网络节点被分配近似相同数量的状态，从而实现良好的加速。许多分布式算法的主要思想是相似的：在网络节点之间划分状态图，即，每个网络节点拥有状态空间的子集。不同之处在于状态空间被划分的方式（划分函数）。例如，在[10，14，1]中已经使用了划分状态空间的概率技术，并且在[2]中提出了一种利用从验证公式导出的因此，在每个网络节点上运行的模型检查算法仅能访问整个系统的一部分。根据算法的类型，它与其他节点通信以实现所需的（全局）结果。Laster（Yorav）和Grumberg [9，16]开发了一种使用模块化的软件模型检查方法他们的模块概念不同于[7，8，3，13]中所理解的模块模型检查中使用的模块概念。这里的模块不是整个系统的一部分，它与其他模块并行运行（即以乘法方式对整个系统做出贡献），而是状态空间的子集，它源于以加法方式分裂整个系统。它的定义遵循程序的语法结构。这种模块的概念也被用在[11]中，其中系统根据程序的语义被拆分除了这种划分，作者在[9，16]中还定义了假设函数的概念，它表示系统的其余部分（由其他部分）提供的关于公式真值的在这篇文章中，我们提出了一种技术，探讨了将Laster和Grumberg的方法扩展到不一定由程序的语法结构产生的分区的可能性，从而允许分布式模型检查。此外，我们修改了模型检查算法，使其可以在分布式环境中运行其主要思想与Laster和Grum- berg提出的思想相似。一旦系统被划分，每个网络节点上的Kripke结构可以包含表示“边界”状态的状态每当模型检查算法到达边界状态时，它使用由其他模型检查算法提供的信息。BRIM、CRHOVA′和Y或AV3∅∀≥∈∈关于网络节点的真实性的公式在那个状态-假设。 作为假设可以改变，通常需要重新计算。有几种方案可以减少所需的重新计算量。在所有情况下，我们还必须考虑相关的通信复杂性。2假设条件下的CTL语义我们的目标是执行一个模型检测算法的n个工作站的集群，称为（网络）节点。除了顺序的情况之外，分区函数f用于在节点之间划分状态空间。在划分状态空间之后，每个节点拥有原始状态空间的一部分对于每个状态s，值f（s）是该状态所属节点的标识符。为了简单起见，我们使用自然数来标识节点。我们将网络节点所拥有的状态空间建模为一个带有边界状态的Kripke结构。直觉上，边界状态是实际上属于其他节点的状态，在Kripke结构中，它们代表状态空间中缺失的定义2.1克里普克结构是一个元组M=（S，R，I），其中S是一个有限的状态集，RS×S是一个转移关系，IS是一个初始状态集。 边界条件为：边界条件（M）={s∈S|我是J。（s，SJ）∈R}.一个Kripke结构M被称为全，如果border（M）=。我们假设整个系统被建模为一个总的Kripke结构M，其中初始状态集合I包含一个初始状态集合。当给定系统被划分时，得到Kripke结构K1，...，K n不需要是完全的。 在第3节中，我们描述了一种特殊的技术，进入K1部分，...，K n.通过划分给定的Kripke结构而产生的Kripke结构被称为片段。M的片段M1是M的子结构，满足M1中的每个状态在M1中没有后继或者它有与M中完全相同的后继的性质。在Kripke结构M中，从状态s0开始的路径π是序列π = s0s1. 使得i0：s iS和（s i，s i+1）R. 最大路径是无限或以边界状态结束的路径。对于最大路径，我们表示为|路的长度。|the length of the path. 如果道路是无限的，|π|= ∞。定义2.2Kripke结构M1=（S1，R1，I1）是Kripke结构M=（S，R，I）i的片段(i)S1是S，(ii) R1R(iii) I1=IS1(iv) 如果s1∈S1，则r（s1，s2）∈R1或s1∈border（M1）.本文考虑一种基于状态的分支时间时序逻辑CTL。BRIM、CRHOVA′和Y或AV4ψA.L→ψψMM定义2.3CTL语言由以下抽象语法定义：：：= p |¬ϕ |ϕ1∧ ϕ2|AX系列|EX-2000|A（101U 102）|其中p的范围是取自集合AP的原子命题。设k为CTL公式。我们用cl（n）表示n的所有子公式的集合，用tcl（n）表示形式为EXn，AXn，E（n1Un2）或A（n1Un2）的n的所有子公式的集合为了定义边界状态下Kripke结构上CTL公式的语义，我们需要修改标准的语义定义。CTL通常在总体结构上解释，而我们的结构通常是非总体的。此外，我们需要在与边界国家相关的假设下定义真理的概念。在这里，我们使用了在[9]中定义的假设下的真理概念的修改。定义2.4Kripke结构M=（S，R，I）和CTL公式φ的假设函数是部分函数A：S×cl（φ）→Bool。我们用符号A（s，n）=n来表示A（s，n）的值是未定义的。通过A，我们表示对所有输入未定义的假设函数。直觉上，A（s，n）=true，如果我们可以假设n在状态s中成立，A（s，n）=false，如果我们可以假设n在状态s中不成立，（s，n）=如果我们不能假设任何东西。让我们用ASM表示Kripke结构M和公式M的所有假设函数的集合。定义2.5设M=（S，R，I）是一个Kripke结构，赋值给每个原子命题一组状态，并给出一个公式。我们定义函数CM：AS→AS. 对于A∈ AS设A=CM（Ain）。则A归纳地定义如下：(i) 概率运算符（ε∈/tcl（ε））：.• A（s，p）=trueifs∈L（p）否则为false如果A（s，1）=true且A（s，2）=true，则为true• A（s，12）=false如果A（s，1）=false或A（s，2）=false否则的话如果A（s，n）=false，则为• A（s，<$1）=如果A（s，n）=true，则为false否则，(ii) 时态运算符（<$∈tcl（<$））：a. 如果s∈border（M），则A（s，n）=Ain（s，n）MBRIM、CRHOVA′和Y或AV5一b. 如果s∈/b或d（M），则A（s，d）定义为以下形式：trueif∀sJ∈S:(s,sJ)∈R⇒A(sJ,ϕ1)=true• A（s，AX<$1）=falseeif<$sJ∈S：（s，sJ）∈R<$A（sJ，<$1）=false否则，trueif∃sJ∈S:(s,sJ)∈R∧A(sJ,ϕ1)=true• A（s，EX1）=falseif <$sJ∈S：（s，sJ）∈R<$A（sJ，<$1）=false否则，如果对于所有路径π=s0s1s2. 其中s=s0n存在一个索引x <|π|使得：[A（sx，n2）=trueor（sx∈border（M）][1][2][3][4][4][5][6][7][8][9][10][11][12][12][13][14][15][16][17][18][19][19]0≤y x：A（sy，1）=true如果在hπ=sss时 存 在 ， 则 会 出 现 错 误 。 . w ith0 1 2• A（s，A（1U2））=s=s0所以你必须要有一<个|π|苏志达（A（sx，A（sy，n2）=false）阿托罗河<|π|：（A（sx，n2）=falseandd1998年 ，|π|= ∞或Ain否则，（个|π| −1，A（1U2））=false））如果存在路径π=s0s1s2. 与s=s0su chthat<|π|苏志达A（sx，n2）=truen（sx∈border（M））和（sx，E（nd<• A（s，E（m1 U m2））=m false如果对于所有路径π= s0s1s2. 其中s=s0你好，<|π|苏志达（A（sx，A（sy，n2）=false）阿托罗河<|π|：（A（sx，n2）=falseandd1998年，|π|= ∞或Ain（s|π| −1，E（1U 2））=false））否则，对于给定的假设函数A，我们定义真值的标准概念M，s| = A as CMBRIM、CRHOVA′和Y或AV6（A）（s，）. 因此，一个状态下的公式的真实性是相对于给定的假设而言的。注意，对于状态s/∈，假设函数A在（s，λ）中的值border（M）不影响CM（Ain）的值 因此，BRIM、CRHOVA′和Y或AV7M∈CMM假设以如下方式与全Kripke结构上的真理的标准概念相关。命题2.6对任意全Kripke结构M，赋值L，CTL公式和假设函数A在∈AS中M，s |= i CM（Ain）（s，）= true注意，在状态s/border（M）中公式的真值取决于π函数。语义函数M的一个重要特征是为片段保留假设。定义2.7设M =（S，R，I）是一个Kripke结构，Ain，A ∈AS n，A ∈ CTL公式. 我们说，A对状态s∈S是正确的，n∈cl（n）（w.r.t. M和Ain）iA（s，n）=CM（Ain）（s，n）我们说A对于状态s∈S（w.r.t.）是正确的M和A在）中，如果对于每个∈ cl（引理2.8设M=（S，R，I）是一个Kripke结构，M1=（S1，R1，I1）是它的片段，Ain，A1∈AS n.如果A1对每个s∈border（M1）（w.r.t. M和A在）则CM1（A1）对每个s∈ S1是正确的。对于引理的证明和所有其他证明，我们参考了本文的完整版本[4]。3分布式CTL模型检测算法在本节中，我们描述分布式CTL模型检测算法。该算法首先在参与的网络节点之间划分给定的状态空间（Kripke结构）这可以根据在网络节点上执行的基本模型检查算法的类型在本地（在网络上）或全局地完成定义3.1设M=（S，R，I）是一个Kripke结构，T∈S。我们定义克里普克结构片段M（T）=（ST，RT，IT）如下：(i) ST={s∈S|s∈TsJ∈Ts.t. （sJ，s）∈R}(ii) R T={（s1，s2）∈ R |s1∈ T，s2∈ S T}(iii) I T={s∈S T|s∈ I}来自T的状态称为原始状态，来自ST\T的状态称为在片段M（T）中的后续结构片段M（T）包含来自T及其所有（直接）后继的状态，以及来自T中的状态的所有转换。初始状态是M中的初始状态。BRIM、CRHOVA′和Y或AV8A∈A（•∈联系我们proc基本节点算法令cl（k）=k1，.，n，z使得n，i，cl（n，j） i，j;fori：= 1tozstep 1do开始案例分析• n=p，p∈AP：对所有s∈S，如果A∈L（s），则A（s，A）：=trueelseA（s，A）：=falseod• i=对所有s∈S，如果A（s，1）=真且 A（s，2）=真，则 A（s，i）：=真;如果A（s，1）=false或 A（s，2）=false则 A（s，i）：=falseod• i=对所有s∈S，do若A（s，1）/=则A（s，i）：=<$A（s，1）odTclTcl对于所有s边界（M）do（s，i）：=in（s，i）od;caseiof• E1=EXE1：对于所有的s∈S\border（M）doifsJ∈S：（sj，sJ）∈RanddA（sJ，1）=truethenA（sj，i）：=true;ifsJ∈S：（s，sJ）∈RA（sJ，1）=falsethenA（s，i）：=falseod• i=AX对于所有的s∈S\border（M）doifsJ∈S：（s，sJ）∈RanddA（sJ，1）=falsethenA（s，i）：=false;ifsJ∈S：（s，sJ）∈RA（sJ，1）=truethenA（s，i）：=trueod• i=E（对于所有s∈S，如果A（s，n2）=真，则A（s，ni）：=真od;当s∈S：A（s，ni）/=真且dA（s，n1）=真且d（s，sj∈S：（s，SJ）∈RanddA（sJ，sji）=truee）doA（s，sji）：=trueodfor alls∈SdoifA（s，sji）=andA（s，sj2）=falsethenA（s，i）：=falseod;当f∈s∈S：A（s，ni）=falseanddA（s，n1）/=falseandd（s，sJ）∈RanddA（sJ，si）• i=A（false）doA（s，i）：=od对于所有s∈S，如果A（s，n2）=真，则A（s，ni）：=真od;当s∈S：A（s，ni）/=真且dA（s，n1）=真且d（s，sJ）∈R<$A（sJ，i）=true）doA（s，i）：=trueod;对于所有s∈SdoifA（s，i）=andA（s，2）=falsethenA（s，i）：=falseod;当f∈S时：A（s，fi）=falseanddA（s，f i1）=/falseandd（s，sJ∈S：（s，sJ）∈R<$A（sJ，<$i）/=false）doA（s，<$i）：=d端欧洲航天公司BRIM、CRHOVA′和Y或AV9结束ODFig.1.改进的模型检测算法BRIM、CRHOVA′和Y或AV10MMC引理3.2设M= （S，R，I）是Kripke结构， 不 ⊆S. 然后片段M（T）是M的片段。分割给定状态空间的结果是一个片段的集合，称为分区。定义3.3设M=（S，R，I）是Kripke结构，f：S→{1，. ..一个分割的Mun-其中，Kf=（K1， .. . ，Kn），则Uchti∈{1， . . ，n}：Ki=片段M（{s∈S|f（s）= i}）。图2示出了系统及其针对分区函数f的 分 区 的 示 例：，s6} → {1，2，3}，f（s1）= f（s2）= 1，f（s3）= f（s4）= 2，f（s5）= f（s6）= 3.边境各州用虚线圆圈标出。在模型检验中，我们感兴趣的是回答M，s| = 0。由于命题2.6，这等价地表示为CM（A）（s，）=true。因此，我们可以通过计算假设函数mc（A）来回答模型检查问题，并在输入（s，A）上返回其值。为了能够分布mc（A）的计算，我们（迭代地）计算仅在系统M的部分上定义的假设函数。我们利用引理2.8来确保这些假设函数等于假设函数mc（A）的假设函数。让我们固定一个全Kripke结构M =（S，R，I），一个CTL公式f，和一个（划分）函数f：S→ {1，.，n}作为算法的输入。此外，委员会认为，让我们表示为K f=（K1，.，Kn）相应的划分，令对于所有i∈ {1，.， n}。图二. 片段分布式算法使用一个过程（节点算法）来计算每个片段Ki上的函数Ki。我们考虑一个显式状态CTL模型检查算法的修改（见[6]），但也可以采用其他模型直观地说，节点算法执行标准的模型检查，但能够也要注意此外，它还计算了I.二三.S1S2S3S4S5S6I.S1S2S3二.S2S3S4S6S5三.S3S5S6BRIM、CRHOVA′和Y或AV11CAL和负面结果，即，如果一个状态s有一个后继者，在这个后继者中，x为真，则可以得出结论，s满足EXx，但它不满足AXx，即使x在s的其他后继者中的有效性还没有得到确定。的图1给出了显式状态节点算法分布式算法的主要思想如下。每个片段Ki由一个单独的进程Pi管理。这些进程在每个网络节点上并行运行。每个过程Pi将假设函数Ai代入下定义的假设函数Ai。在初始化之后，它计算（使用节点al-出租m）函数M（i）。然后它将结果发送给每个进程P可能对它们感兴趣（即，它发送P重复这些步骤，直到达到一个固定点（在稳定化之后，仍然可以保留状态s和公式m，其中Ai（s，m）=m。这可能发生在U操作符的情况一种可能的情况如图3所示状态空间具有在三个网络节点上均匀分布的三个状态S={s1，s2，s3}假设赋值使得L（p）=S且（q）=。如果我们想要模型检查公式=A（pUq），则每个节点算法到达定点，边界状态下未定义值三.图3.第三章。未定义的假设然而，如果在所有节点的所有状态下都已经计算出了π的所有子公式的真值，那么从已经达到定点的事实，我们可以得出结论，π在s中不成立。因此，所有进程都推断此信息并继续计算。在我们的例子中，这得到的答案是，在S的任何状态下，都不成立。重复所描述的计算，直到我们正在搜索的信息分布式算法的主要思想总结在图4中。我们现在详细阐述分布式算法，以便能够讨论其正确性。图5给出了详细的伪代码。请注意，在算法的执行中有两个主要阶段。在I.二s1s2S2I.S1S2二.S2S3三.S3S1BRIM、CRHOVA′和Y或AV12一联系我们×≤×procDistritedAlgorithm（iputt：toalKSM，m，f;utputt：f（sM）（sM，m））将M分割成Ki;对于所有i 1，.，n 并行地做对于所有Ki取初始假设函数;重复重复尽你所能计算;向其他节点发送相关信息;从其他节点接收相关信息;直到所有过程达到定点;外推额外信息;直到全部计算完毕;为初始化状态恢复;奥德恩德见图4。 分布式算法在第一阶段，这些过程重复地计算关于公式的真值的信息，并且分别向其他过程发送计算的信息和从其他过程接收计算的信息。当达到一个固定点时，此阶段结束。然后执行第二阶段，当每个过程利用已经达到定点的事实来推断信息时。这两个阶段重复执行，直到计算出我们搜索的信息。让我们分别表示第一和第二阶段点I和II的开始，如算法中所标记的。当到达定点时，算法正好在点II。在第一阶段的开始没有同步，但不失一般性，我们可以假设所有进程都同时开始第一阶段。对于每个状态和每个公式，我们要说它的值是否已经被计算出来了。我们考虑一个状态的值和一个计算公式，如果对于某些i，Ai的适当值已经被定义。 在达到在第一阶段结束时的定点，可能需要解决未确定的值能够在计算中继续，即，将某个状态和某个公式的值视为计算值。我们选择一个公式是“最低”子公式的对让我们用Def来表示已经在这个意义上计算过的来自S cl（n）的所有元组的集合，Undef是它的补数。从形式上讲，Def={（s，ε）∈S×cl（ε）|i∈{1， . . ，n}：Ai（s，n）/=n}Undef是在S×cl（n）中Def的补数。现在，让我们定义一个关于S cl（n）的排序 它将Undef中最小的元组。定义3.4设s1，s2∈S，s1，s2∈cl（n）。然后（s1，n1）≤（s2，n2）惠1∈cl（n2）BRIM、CRHOVA′和Y或AV13AA一--AAod;一∈}1 Proc2将M分解为Ki;3对于所有i ∈ {1，. ，n}并行执行4{ProcessPi}5i：=0;6重复7第一阶段：8重复9AJi：=CKi（Ai）10对所有的ε∈tcl（ε），s ∈Si：s在Ki中是原始的，在Kj中是后继的11如果AJi（s，n）/=n，且 Ai（s，）=12然后将AJi（s，n）发送给进程Pjod;13对于所有接收到的Aj（s，n），做AJi（s，n）：=Aj（s，n）od;14i：=Ji15直到所有进程都达到固定点;16{stageII：}17对所有的ε∈{E（ε1Uε2），A（ε1Uε2）}，s ∈border（Ki），18如果（s，n）在Undef中最小，则Ai（s，n）=falseod19untilAi（s，n）/=n，n∈cl（n），n∈Si2021returnf（s）（s，）22 端图五. 计算CM已经到达定点的事实不能在本地检测到。然而，通过使用计算机之间的额外通信，我们能够确定它.进程之间还需要进行额外的通信，以找出Undef中哪些元组（s，n）是最小的（第18行）。假设一个定点有已经到达。每个进程P i计算一个由元组组成的集合LocalyMinimali，这些 元 组 在 A i 未 定 义 的 集 合 中 是 最 小 的 。 当 完 成 时 ， 它 发 送estLocalyMinimalF或mulasi={A∈{A（1U2），E（1U2）}|s∈S i：（s，n） LocalyMinimali到每个其他进程，并从其他进程接收类似的信息。使用此信息，每个进程都能够确定来自LocalyMinimali的哪些元组在Undef中是最小的。（注意，如果一个元组不在LocalyMinimali中，那么它在Undef中就不能是最小的）。为了提高算法的性能，我们可以使其在到达某个时刻时停止f（s）（s，s）是可计算的，即，如果我们之前已经计算了所需的信息，则不需要读取固定点。4算法的正确性在本节中，我们陈述分布式算法的正确性，即，我们证明了一个算法总是停止并返回值Af（s）（s，s），其中s等于CM（A）（s，s）. 我们提出的原则只适用于关键词，而不适用于其他词BRIM、CRHOVA′和Y或AV14证明我们指的是文件的完整版本[4]。第一个引理指出，在第一阶段完成后，所有到目前为止计算的假设都是正确的。Lemma4. 1假设计算在点I（第7行）处，并且i∈{1， . . ，n}，s∈S，n ∈cl（n），则以下性质成立：Ai（s，n）/= n意味着Ai（s，n）是正确的（w.r.t. M和A）那么这个性质在点II（第16行）也成立下一个引理表达了这样一个性质，即具有定义值的假设以统一的方式分配真值。Lemma4. 2假设该算法在点II处，并且m∈{1， . . ，n}，s∈cl（n），则Ai（s）=/n蕴涵Ai（s）isc or rect（w. R. t.M和A）。设s∈S，n∈cl（n）s.（s，n）∈Def. 然后要么i∈{1， . . ，n}：s∈Ki<$Ai（s，n）=true或i∈{1， . . ，n}：s∈Ki<$Ai（s，n）=false引理4.3陈述了分布式算法的关键思想。 在达到在分布式计算中的fixpoint，Undef中仍然可能存在一个元组，这意味着对于某些状态和某些公式，假设值仍然是unfined。这是包含U运算符的公式的情况。在节点算法中，当声明U公式不成立时，计算最大定点。但要正确计算最大定点，探索整个状态空间，这在分布式环境中是不可能的（节点算法仅能访问整个系统的一部分）。另一方面，当声明U公式成立时，计算最小定点，并且可以以分布式算法工作的方式迭代地仅在状态空间的一部分上执行这样的计算。因此，如果在Undef中有一个元组，使得它在到达分布式计算的定点时在这个集合中是最小的，那么这个公式在整个系统中的状态下都不成立我们对索赔提出了充分的证据Lemma4. 图3算法的一个例子是，hm的计算是在点II处，{1， .. . ，n}，s∈cl（n），则Ai（s）n ∈Cl（n）成立，Ai（s）n∈ C l（n），其中Ai（s）是正确（w.r.t. M和A）。还假设存在s ∈ S，n ∈ cl（n）故（s，n）在Undef中是最小的。 则CM（A）（s，）= false。证据 我们把证明分成几部分。• 我们首先证明了该公式必须是U-公式，即，A = A（1U 2）或A=E（ 1U2）。我们用反证来证明这个主张.假设A/=A（ 1U2）且A/=E（1U2）。 我们证明，如果必须存在i ∈ {1，.，n}，使得可以计算函数Ai（s，n），其是与达到固定点的假设相矛盾。BRIM、CRHOVA′和Y或AV15CAACAC≤ CA∀ ∈ ∀ ∈/∈注意到SJS，证明了（SJ，n）Def作为（s，n）在Undef中是极小的.设i=f（s），意味着s在Ki中是原始的。因为M是总数，s∈/border（Ki）.- 设P=P。那么它就可以简单地计算出来。- Let=<$1或=<$1<$2。CKi（Ai）（s，n）可以用计算机计算Ai（s，j）定义为j=1，2。- 设λ =EXλ1或λ =AXλ1。让s1，.，st都是s在M中的后继者。因为s是K i中的原始值，所以我们有s1，.，st∈ Ki. 此外，对于所有j ∈{1，...，t}，并且由此可以得出CKi（Ai）（s，）可以是计算。• 我们现在证明如果E = E（<$1U <$2）和CM（A<$）（s，<$）=真则存在SJ∈ S使得（SJ，<$）∈ U ndef可以计算。当我们假设已经达到固定点时，我们得出结论CM（A）（s，）= false。从M是全的这一事实，我们有CM（A）（s，）=truei存在一条路径π= s0s1s2. 其中s= s0和x<|π|：这样，CM（Ain）（sx，2）=真且0≤y x：CM（Ain）（sy，1）=真。设k是最大数，使得k≤x且（sk，n）∈Undef.这样一个数存在，因为我们假设（s0，n）∈Undef且肯定0≤x。设i=f（sk）是对sk为原始.假设k=x。从（s，）在Undef中是极小的这一事实，我们有（sk，2）∈Def。根据引理4.2，我们得出结论，Ai（sk，k2）/=k，并且根据已经计算的值是正确的假设，我们最终有i（sk，k2）=true。这允许计算Ki（i）（s k，k）=真的假设k x.我们知道sk+1∈Ki和（sk，sk+1）∈Ki，因为sk在Ki中是原的.此外，Ai（sk+1，n）/=n（从k的最大性）和Ai（sk+1，n）=真（从计算的正确性的假设价值观）。同样，它允许计算Ki i（s k，k）= true。在这两种情况下，我们都有矛盾，因此我们可以得出结论，CM（A）（s，）=false.• 现在设A=A（A1U2）。我们将遵循与前一个案例类似的想法让我们假设CM（A）（s，）=真，我们将展示与到达定点的利用M的全性，我们有CM（A）（s，）= true i对于所有路径π=s0s1s2. 如果s = s0，则存在x<|π|使得CM（A）（s x，2）=真且0

下载后可阅读完整内容，剩余1页未读，立即下载