一阶逻辑与最小不动点逻辑的算法复杂性评估

15X网址：http://www.elsevier.nl/locate/entcs/volume67.html20页模型检查游戏ErichGradel1亚琛工业大学摘要我们调查评估游戏的一阶逻辑和最小不动点逻辑，并讨论其算法的复杂性。关键词：逻辑，博弈，模型检测，xed点逻辑，奇偶博弈，复杂性1逻辑与复杂性在计算机科学中的许多逻辑领域，人们对逻辑的常见推理任务的算法复杂性感兴趣。有许多这样的任务，但其中大多数可以很容易地减少到两个（至少对于具有合理闭包属性的逻辑），即满意能力测试和模型检查。逻辑L和结构域D的满足性问题，以公式2L为输入，所要回答的问题是D中是否存在一个模型。模型检验问题（对于D上的L）要求，给定结构A2D和公式2L，是否Aj=。一个密切相关的问题是公式计算（或查询计算）：给定一个结构，A和一个公式 （x）（有自由变量），计算由下式定义的关系：在A上，即， 集合A：= f a：A j=（a）g. 显然，评估问题的公式与k个自由变量的结构与n个元素减少到nk模型检测问题。请注意，模型检查问题有两个输入：结构和公式。我们可以根据两个输入来衡量复杂度，这就是通常所说的模型检查问题的组合复杂度（对于L和D）。然而，在许多情况下，两个输入中的一个是固定的，我们只根据另一个来衡量复杂性。如果我们对一个结构A进行模型检验，那么L在这个结构上的模型检验问题就相当于判定A的L -定理ThL（A）：=f2L：Aj=g. 的1 Mathematische Grundlagen der Informatik，RWTH Aachen，52056 Aachen，Germany.电子邮件地址：graedel@informatik.rwth-aachen.de网址：www-mgi.informatik.rwth-aachen.de/~graedel2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。16一这个问题的复杂性也被称为模型检验问题的表达式复杂性（对于LonA）。特别是对于一阶逻辑FO和一元二阶逻辑MSO，这样的问题在逻辑中有着悠久的传统和众多的应用。 对于许多领域（包括nite模型理论和数据库）更重要的是固定公式的模型检验问题，这相当于确定内部D的模型类，M odD（）：=fA2D：Aj=g。 由于它与数据库的相关性，这个问题的复杂性也被称为模型检测问题的数据复杂性（对于D）。几乎任何逻辑的模型检查问题都可以被转换为适当的模型检查游戏（也称为Hintikka游戏）的策略问题。对于任何公式（x），任何结构A（与相同的词汇），以及对A的任意元素元组，构造一个Hintikka对策G（A;（a））. 是由两名球员扮演，韦里尔和法尔西尔。 Veri er（有时也称为参与人0、9或Eloise）试图证明Aj=（a），而Falsi er（也称为参与人1、8或Abelard）试图证明公式为假。对于一阶逻辑，评价博弈非常简单，因为获胜条件是位置性的，并且博弈是有根据的，即，所有可能的播放都是NITE（不管输入结构是NITE还是IN NITE）。对于更强大的逻辑，特别是xed-point逻辑，模型检查游戏可能会有更复杂的获胜条件。2一阶逻辑设A是一个nite结构，（x）是一个关系一阶公式，我们假设它是否定范式，即， 由原子和否定原子通过命题连接词^;_和数量词构建而成9; 8.因此，任何一阶公式都可以有效地转化为一个等价的负范式公式。 模型博 弈 G （ A;（ a） ） 具有这 样 的 位置 （“;） ，即”是，和的子模型！ A是从'的自由变量到A的元素的赋值。为了简化表示法，我们通常将位置（';）写成'（b），其中将元组b赋给'的自由变量。博弈的初始位置是（a）。验证者（参与人0）在与析取和以存在量化器开始的公式相关联的位置移动。从位置“_#她移动到"或#。从位置9y'（b;y）Ve r i er可以移动到ny位置'（b;c），其中c2A。对偶地，Falsi er（Pl ayer1）在合取和万有量化上作相应的移动。原子或否定原子，即， 形式为b=b0，b6 =b0，Rb，或r：Rb的位置（b），博弈结束。 如果Aj=“（b），则V在平面上有w，否则F也有w。模型检查游戏是一种定义逻辑语义的方法。与标准定义的等价性可以通过一个简单的归纳来证明命题2.1Aj=（a）当且仅当Veri er有获胜策略17对于博弈G（A;（a））。这表明了一种基于博弈的模型检验方法：给定A和，构造博弈G（A;），并决定Verier是否具有从初始位置开始的获胜策略。因此，让我们更仔细地研究一下博弈的策略3夜间游戏的策略问题。抽象地说，我们可以用一个有向图G =（V; V 0; E）来描述一个具有位置获胜条件的两人博弈，其论域V是位置的集合，其中V 0 V是参与者0移动的位置的集合，其中EVV 就是一系列的动作通过V 1：= V我们表示为参与人1的移动位置对于任意位置v2V，设v E：=fw：（v;w）2E g表示v的后继集.为了描述获胜条件，我们采用了这样的约定，即参与人i在位置v2Vi处输了，在那里没有移动是可能的（即，vE=;）.或者，可以明确地在游戏描述中包括每个玩家的获胜终端位置的集合S0;S1博弈G是两个参与人从给定位置v 0开始形成的路径v 0 v 1：。 在位置vn2V0，Pl ayer0选择移动e（vn;vn+1）2E，在位置vn2 V1，参与人1选择移动.当在当前位置没有可用的移动时，必须选择的玩家输了。如果这种情况从未发生，比赛将在夜间进行，获胜者必须通过在夜间比赛中获胜的条件来确定目前，让我们说，在夜间发挥是赢得了没有一个球员。一个玩家的策略是一个函数，它为每一种情况定义一个移动，一出他必须移动的戏特别有趣的是位置策略，它不依赖于游戏的历史，而只依赖于当前的位置。因此，参与人i在G中的位置策略是函数f：Vi！ 表示每个位置v 2 Vi的选择（v;f（v））2E。一个pl ayv0v1 ：与一个Pl ayeri的位置策略f一致，如果对所有vn2Vi，vn+1=f（vn）. 一个玩家的策略是从位置v0获胜，如果他从v 0开始赢得每一场比赛，这是与该策略一致的。我们说一个策略在集合W上是赢的，如果它在W中的每个位置都是赢的。给定一个博弈G，我们用Wi（i= 0; 1）表示参与者i从其开始有获胜策略的位置集合。如果一个游戏的所有玩法都是nite的，那么这个游戏就被称为well-founded。例如，一个一阶模型博弈G（A;（a））的博弈图是nite当且仅当A是nite，但这个博弈在任何情况下都是良基的。然而，一般来说，具有nite游戏图的游戏不需要是有根据的。一个博弈被称为确定的，如果从每个位置，一个玩家有一个获胜的策略，即，如果W0[W1=V.有根据的博弈总是确定的，大类更一般的博弈（如18我我我我我我u n直到Wn+1=Wn。Borel层次结构，参见[11，12]）。我们用博弈来表示博弈的策略问题（具有nite博弈图和位置获胜条件），博弈=f（G;v）：Player0在G中有一个获胜策略，来自posituationv g：显然，博弈问题可以在多项式时间内解决：用Wn表示参与者i有获胜策略的位置集合最多只能走n步然后W0=fv2V1i：vE= ;g是集合参与人i的获胜终端位置，我们可以计算出归纳地，Wn+1：=fv2 V ：vE\Wn6=;g[fv2V ：vEWng我我要知道博弈实际上可以在线性时间内求解，还需要做一些工作。下面的算法是深度- rst搜索的一个变体，并且在时间O（jV j + jE j）内计算两个玩家的整个获胜集。定理3.1 nite对策的获胜集可以在线性时间内计算。证据我们提出了一个算法，计算每个位置，哪个球员，如果有的话，有一个获胜的策略，从这个位置开始的游戏。在计算过程中，使用了三个数组：win [v]包含0或1，表示哪个玩家获胜，或者？如果我们还不知道，或者如果没有参与人有一个胜利的战略，从v;P [v]包含v的前代;n [v]是其中win[ v ] =？的后继者的数量。对策问题的线性时间算法输入：对策G=（V;V0; E）对于所有v2 V do（1：initialisation）win[v]：=？[v]：=;n[ v]：= 0结束对于所有（u; v）2Edo（2：计算P和n）P[v]：= P[v][f ugn[u]：=n[u]+1enddo0119对于所有v2V0（3：计算赢）如果n[v] = 0则计算（v，1）对于所有v2VV0如果n[v] = 0，则返回绕组结束程序重复（v， i）如果wi n[v]6=？然后返回win[v]：= i（4：mark v as winning for Player i）for allu 2 P [v] do（5：将更改传播到previously）n[ u]：= n[ u] 1如果u2Vi或 n[ u] = 0，则将（ u， i）enddo端这个算法的核心是过程callate（v; i），每当我们发现参与人i从位置v有获胜策略时，都会调用这个过程。martate（v; i）记录了这一事实，并研究我们现在是否能够确定v的任何前辈的获胜者。这是通过应用以下规则来实现的：如果前任u属于参与人i，那么这个参与人有一个获胜策略，移动到位置v.如 果前任u属于对手，win[u]是未知的，并且已经确定了所有继任者w的获胜玩家，那么对于所有这些继任者，win[w] = i，并且玩家i从u获胜，而不管他的对手的选择。由于对于每个位置v，仅到达部分（4）和（5）一次，所以（5 ）中的loop的内部部分最多执行Pvj P[v] j =j E j次。因此算法的运行时间为O（jVj+jEj）。分配给win[v]的值的正确性通过对相应玩家可以确保他获胜的移动次数的直接归纳注意，在第3部分中满足n [ v ] = 0的位置恰好是那些没有向外边缘的位置，如果n[v]是由y_ded_y_ded。2博弈是一个P时间完全问题（见[7]）. 这仍然是严格交替博弈的情况，其中EV0V1[V1V 0]。实际上，任何博弈都可以转化为等价的严格交替博弈，通过为每个（u;v）2ViVi引入一个新的ndee2V1i，并通过用两个移动（u; e）和（e; u）替换移动（u; v）。博弈问题（有时也称为交替可达性）是一个一般的组合问题，在许多领域以不同的形式出现。为了说明这一点，通过一个例子，我们表明命题霍恩公式的满意性问题本质上是相同的问题作为游戏。20Horn公式的满足能力。众所周知，命题Horn公式的满意性问题Sat-HornPtime-complete [7]，以及在线性时间内可解[3，8]。使用博弈问题，我们得到非常简单的证明这两个结果。事实上，Game和Sat-Horn在对数线性约简下是等价的，即，可以用线性时间和对数空间计算的约简简化是如此简单，以至于我们可以说游戏和Sat-Horn实际上是同一个问题。定理3.2 Sat-Horn与博弈是对数线性等价的。是的。 在一个有限对策图G=（V;V0;E）中，我们可以在时间O（jVj+ jEj）内构造一个命题Horn公式 G ， 它 由子句uv和子句uv 1 ^ ^vm组成，子句uv对所有边（u; v）2 E，其中uE=fv1; ：;vmg. G的最小模型恰好是参与人0的获胜集合W 0。因此，如果霍恩公式G^（0v）不满足，则v2W0.Sat-Hornloglin游戏：GivenaHornformula（X1; ：;Xn）=Vi2ICi具有命题变量X1;：;Xn和形式Hi的Horn子句CiXi1 ^^Xim（其中，子句的头部Hi是比例变量或常数0），我们如下定义博弈G。参与人0的位置是初始位置0和命题变量X 1;：; X n，参与人1的位置是的子句。参与人0可以从位置X移动到任何以X为中心的子句C，参与人1可以从子句C移动到C主体中出现的任何变量。形式上 ， G = （ V; E ） ， V = V 0[V 1 ， 其 中 V0=f0g [fX1; ： ： ;Xn g ，V1=fCi：i2I g，并且E= f（ X; C）2 V0V1： X=压头（ C）g[ f（ C; X）2 V1V0： X2体（ C）g：当且仅当j=X时，参与人0在位置X上对G有获胜策略。特别地，当且仅当Pl ayer0从位置0获胜时，是不满意的。24复杂一阶模型检验模型博弈G（A;）的规模约为A的子公式的不同实例的个数。为了尽可能精确地测量博弈的大小以及模型检测复杂度的时间和空间界限，除了公式长度jj之外，我们还使用以下参数。闭包cl（）是.显然，jcl（）j在某些情况下，jcl（）j可以比J 2019 - 05 - 22 00：00： 00 00：00 ）是量化器的最大嵌套深度的宽度是子公式中自由变量的最大数量，即，width（）=maxfjfree（'）j：'2cl（） g：21我们也可以用尽可能少的变量重写公式，而不是考虑宽度。引理4.1一个一阶公式有宽度k，当且仅当它通过重命名绑定变量等价于一个至多有k个不同变量符号的一阶公式。逻辑的有界变量片段已经受到了很多关注，尼特模型理论然而，我们在这里的状态结果的公式宽度，而不是变量的数量，以避免必要的节约变量的数量。在许多情况下，显式地构建完整的模型检测博弈，然后解决策略问题并不是最好的方法，因为实际上并不需要博弈的许多位置。此外，由于交替算法实际上是游戏，因此对模型检查游戏复杂性的最佳估计通常是交替复杂性类。我们提出了一个交替的模型检测算法的一阶逻辑，可以被看作是一个模型检测游戏，而玩它的Y结构。定理4.2有一个交替的模型检验算法，给定一个nite结构A和一个第一阶句子，决定是否Aj=在时间上O（j j + qr（）log jAj）和空间上O（j j+ width（）log jAj）（假设原子语句在常数时间内求值）。证据我们提出了一个递归交替过程ModelCheck（A; ;），它给出了A，一个可能包含自由变量的公式和一个赋值：free（）！A，决定是否Aj=[]。ModelCheck（A;; ）的方式输入：一个否定范式的一阶公式，一个nite结构A（具有论域A），一个赋值：free（）！如果是一个原子或否定原子，那么如果Aj=[ ]accept elserejectif=_#然后做guess'2f;#g，设0：=jfree（“）ModelChe ck（A;0;”）如果=#然后做f;#g，且设0：=j free（“）M odelChe ck（A;0;”）如果=9x'然后做猜想A中的一个元素aM odelChe ck（A;[x7！a];'）if=8x'，则22我我普遍地选择AM odelChe ck（A;[x7！a];'）一个简单的归纳表明这个过程是正确的。该过程所需的在每个计算路径上，必须选择A的至多qr（）个元素，并且每个元素需要log j A j比特。时间复杂度为O（j j + qr（）log jA j）。在评估期间，算法需要维持指向当前位置的指针，并且存储当前分配，这需要用于当前子算法的空闲（“）logj Aj比特。 因此，算法所需的空间是O（j j +width（）log j A j）。2定理4.3一阶逻辑的模型检验问题是P空间完全的。对于任意给定的k2，宽度不超过k的一阶公式的模型检验问题是P时间完全的.证据这些复杂性类中的成员资格直接从定理4.2通过交替多项式时间与多项式空间一致以及交替对数空间与多项式时间一致完备性是从已知的完备问题直接还原而来的。定量布尔公式的求值问题QBF，归结为固定结构（A; P）上的一阶模型检验问题，其中A=f0; 1g ， P=f1 g. GivenaquantiedBorandomformula ， withoutfreeprop-sitional variables ， translate it into a rst order sentence as follows ：replaceeveryquanti cation9Xi 或8Xi对于比例变量Xi， 通过相应的一阶量子化9xi或8xi并替换原子位置X由y原子组成。 O b=0，当且仅当（A;P）j=0。这证明了表达式复杂度和组合复杂度一阶模型检验是Pspace完备的。为了证明宽度为2的一阶公式的模型检验问题是P时间完全的，我们将严格改变博弈的博弈问题简化为P时间完全的，其中参与者0移动 rst。对于n2N，我们构造归纳公式n，0（x）：= 8 y： Exy2n+1（x）：=9y（Exy^2n（y））2n+2（x）：=8y（Exy！2n+1（y））：显然n的宽度为2，对于任何严格的交替博弈G=（V;V0; E），参与人0可以在从位置v2V0（对于奇数n）或v2V1开始的（对于e venn）当且仅当Gj=n（v）。 现在，如果Pl ayer0有一个从v 2 V 0开始的获胜策略，那么她也有一个在最多n步中获胜的策略，其中n = j V j，因为否则游戏将陷入循环。23X因此，博弈问题的任何实例G;v（对于v2V0的严格交替博弈）都可以简化为宽度为2的一阶公式的模型检验问题的实例G;n（v）2P时间完备性的论证事实上已经适用于命题模态逻辑ML [6]. 用y'0：=2fals e，'2n+1=32n，和'2n+2：=2'2n+1定义的模来代替上面构造的公式n（x）。推论4.4 ML的模型检测问题是P时间完全的.如果我们考虑一个固定公式，定理4.2告诉我们，一阶逻辑的数据复杂度远低于表达式或组合复杂度。推论4.5对于每个第一阶句子，fA：Anite;Aj= g 2Alogtime. 特别是，任何固定的一阶句子的评价问题可以用对数空间确定性地计算。5至少X点逻辑不动点逻辑通过构造器扩展了基本的逻辑形式（如一阶逻辑、连接查询或命题模态逻辑），用于形成关系运算符的不动点。 注意，任何公式（R; x），vocabu-lary[fR g]和一个长度与R，定义了对每个-结构A，一个更新算子F：P（Ak）！P（Ak）上的k元关系类，即F：R7！fa：（A; R）j=（R; a）g：如果R恰好在中只出现正值，则算子F是单调的，在这种情况下，它有一个最小固定点lfp（F）和一个最大固定点gfp（F）。最小和最大固定点也可以归纳地构造算子F的阶段是集合X（序数），定义为：X0：=;;X+1：=F（ X）;以及X：=[X对于极限序数：<单调算子的阶段序列是递增的，因此最终到达一个固定点，该点与最小固定点重合。 最大的固定点可以通过对偶归纳来构造，从Y0= Ak ，设置Y+1个：=F（ Y），Y=TY<极限序数的这些阶段的递减序列，然后最终收敛到最大定点Y1 = gfp（F）.24X一引理5.1设F：P（A k）！P（Ak）是有限集合A上的单调算子. 如果F是在多项式时间内可计算的（w.r.t. jA j），则定点lfp（F）和gfp（F）也是如此。最小定点逻辑，记为LFP，是通过在一阶逻辑的语法中添加以下最小定点形成规则来定义的逻辑：如果（R; x）是词汇表[fR g]的公式，其中只有R，if是变量的元组，t是项的元组（使得并且t匹配R的arity），则[lfp Rx：]（t）和[ gfp Rx：]（t）是词汇的公式。这些公式的自由一阶变量是（free（）f x：xin x g）[free（t）.语义 任何 - 结构A，为所有自由变量提供解释-在公式中，我们有Aj= [lfp R：]（t）if t（The tuple of）解释t）的A的元素包含在lfp（F）中，其中F是A上由定义的更新运算符。对于最大的固定点也是如此。例5.2下面是一个xed点公式，它定义了二元谓词E的传递闭包：TC（u;v）：=[lfpTxy：Exy_9z（Exz^Tzy）]（u;v）：注意，在公式[lfpRx：']（t）中，除了x中的自由变量之外，还有其他自由变量，这些变量在定点公式中保持自由。 它们通常被称为定点公式的参数。例如，传递闭包也可以由以下公式定义：'（u;v）：=[lfpT y：Euy-9x（Tx^Exy）]（v）其中u为参数。很容易看出，每一个LFP公式都等价于一个没有参数的公式（以增加定点变量的数量为代价）。例5.3博弈问题是LFP可定义的，by[lfpWx：']（x），其中'（W;x）：= （ V0x^9y （ Exy^Wy ） ） _ （ ： V0^8y （ Exy ！Wy））：博弈在LFP中起着重要的作用。可以证明，每个LFP-可定义的问题都可以通过无量化翻译归结为博弈。因此，通过这种归约的概念，博弈对于LFP是完全的，因此如果试图从LFP中分离出较弱的逻辑，那么它是一个自然的候选者。LFP的一个更一般的变体允许在几个公式上同时归纳。设1（R;1）; ：;m（R; m）be用于vocabulary[fR1; ： ：;Rmg，XXXX25X其中只有R1; ：;Rm的概率，并且令对于每个chim，ibea26X不一>>><变量序列匹配的arity的Ri。然后8S：=R11：=1.：>Rmm：=m是更新规则的系统，其用于构建公式[lfpRi：S]（t），并且[gfpRi：S]（t）（对于长度与Ri的arity匹配的任何项的元组）。语义：S定义一个单调操作器SA=（S; ：; S）映射元组1mR=（R; ：; R）A（R）=（S（R）; ：; S（R）其中1米1米Si（R）：=fa：（A;R）j=i（R;a）g. 由于算子是单调的，在lfp（SA）=（R1;R2;R3;R4）中，（A）如果2R1，则N=[lfpR：S] 。1米ii同样对于最大的 固定点。虽然同时固定点并不比简单固定点提供更多的表达能力，但它们允许以更模块化和更可读的形式编写公式。最小和最大定点之间的对偶性意味着对于任何公式，[gfpRx：]（t）：[lfpRx：：[R=：R]]（t）其中[R=：R]是通过用R原子的负原子代替R原子的所有同现而得到的公式。(As R仅在中为正，对于[R=：R]也是如此）。 由于这种双重性，在LFP的定义中，最大端点常常被省略。另一方面，有时保持最大不动点是方便的，并使用对偶性（和德摩根定律）将LFP公式转化为否定范式，即，把负离子一直推到原子。从一阶运算是多项式时间可计算的这一事实，以及从引理5.1，我们立即得出结论，nite结构的每个LFP可定义的性质都是多项式时间可计算的。第5.4章让我们在LFP中在多项式时间内可判定给定的nite结构A是否是简而言之：LFP Ptime。模态演算。LFP的一个片段，在计算机科学的许多领域都具有根本的重要性（例如， 在控制器综合、硬件验证和知识表示中）是模态演算L。它是通过在命题模态逻辑ML上增加最小和最大固定点而换句话说，L与ML的关系就像LFP与FO的关系一样。定义5.5模态演算L通过以下规则扩展ML（包括命题变量X; Y;：，其可以被视为一元二阶变量）以用于构建定点公式：X27一一如果是L中的公式，X是只在中正出现的命题变量，则X：和X：也是L-公式。这些定点公式的语义完全类似于LFP的语义。在一个过渡系统G（具有论域V，并对其他自由二阶变量进行解释，除了X之外，还可以有）定义单调算子F ：P（V）！P（V）赋值给每个集合XV集G（X）：=f v 2V：（G; X）;v j=G. 现在G; vj=X：i v2 lfp（ F） G; vj= X：iv2gfp（ F）对于LFP，在不改变表示能力的情况下，也可以同时给出更新规则系统S的定点公式（X：S）和（X：S虽然ML和L被定义为命题逻辑的扩展，但将它们分别视为FO和LFP的片段通常更方便实际上，模态公式定义了一个关于变迁系统的查询，将节点集[[]] G =f v：G; v j= g与G相关联，并且这个集合可以等价地由FO-或LFP-公式（x）定义。这个转换将一个原子命题Pb转换为原子Pb x，它与布尔连接词交换，并将模态算子转换为量化算子，如下所示：（ha i）（x）：= 9 y（E xy^（y））（[a]）（x）：=8y（E xy！（y））：最后，形式X：'的公式被转换成[lfpXx：']（x），对于最大的固定点也是如此。请注意，结果公式的宽度为2，因此只能用两个一阶变量来写。命题5.6对于每个公式2 L，存在一个公式（十）2宽度为2的LFP，相当于在这个意义上，G; v j=我G j=（v）.让我们转向算法问题。 L的模型检查问题的复杂性是一个主要的开放问题，就组合复杂性和表达式复杂性而言（见第6节）。然而，数据的复杂性可以很容易地解决。命题5.7（L的数据复杂度）修正任何公式2L给定一个nite转移系统G和一个节点v，它可以在多项式时间内决定G; v j=.进一步地，存在2个L， 使得模型检验问题是P时间完全的.证据由于L是LFP的片段，第一个声明是显而易见的。 对于第二个要求，回想一下严格交替博弈的博弈问题是P时间完全的. 从位置v2v0开始，玩家有一个获胜的策略 在博弈中G=（V;V0;E）当且仅当G;vj=X：32X。228关于-演算的更多信息，参见[1，2]和那里的参考文献。6最小固定点逻辑对于最小不动点逻辑，适当的评估游戏是奇偶游戏。这些是可能在夜间持续时间的游戏，其中每个位置被分配一个自然数，称为其优先级，并且在夜间游戏的获胜者根据在游戏期间经常看到的最低优先级是偶数还是奇数来确定。奇偶博弈的获胜集和获胜策略是否今天已知的最好的算法在游戏的大小上是多项式的，但在优先级的数量上是指数的。用于模态演算的实际竞争性模型检查算法通过解决相关联的奇偶博弈的策略问题来工作（参见，例如，[10]）。定义6.1一个偶对策由标号图G=（V;V0; E ;）给出，其中（V;V0;E）是第2节中的对策图，并且：V！ N为每个位置分配一个优先级。博弈中不同优先级的个数是G的指数。回想一下，游戏的夜间游戏被卡住的玩家输掉，即，不能动。与第二节博弈的区别是我们有不同的获胜条件，在夜间计划v0v1v2： 。 如果在优先级的序列（v0）（v1）：中最小的numb是偶数，则参与人0赢得比赛，否则参与人1获胜。奇偶博弈的遗忘决定性定理[5]指出，这些博弈总是确定的（即，从每一个位置，其中一个参与者都有一个获胜的策略），事实上，位置策略总是有效的。读者可以参考[16]或[13]。定理6.2（遗忘决定性）在任何奇偶博弈中，位置集可以分成两个集合W0W1 使得参与者0在W0上具有概率获胜策略参与人1在W1上有一个概率获胜策略。定理6.3在NP\Co-NP中可以决定在一个奇偶博弈中给定的位置是否是参与人0的获胜位置。是的。 在一个部分博弈G=（V;V0;E1）中，如果存在一个位置策略f：Vi，则v是参与人i的获胜位置！从位置v胜出。因此，它表明，问题是否一个给定的f：V i！V是参与人i从位置v开始的获胜策略可以在多项式时间内决定。我们对参与人0证明了这一点;对参与人1的论证是类似的。Gi venGandf：V0！ 通过只保留与f一致的移动，即，Ef=f（v;w）：（v2Vi^w=f（v））_（v2V1i^（v;w）2E）g：29我我我们定义一个分解T = T[ T]，其中T是v 2 T的集合，其中0T+1：=fv 2 T：s（v）2Wg00<在这个简化博弈中，只有对手，即参与人1，会采取重要的行动。我们称（V; E f）中的一个圈为奇数，如果它的节点的最低优先级是奇数。显然，Pl ayer0通过策略f从位置v赢得G，当且仅当，在Gf中没有odd循环且没有终止位置w2V0 可以从v. 由于可达性问题在多项式时间内是可解的，因此该声明如下。2事实上，Jurdzinski[9]提出了问题是在UP\Co-UP中，其中UP表示具有唯一证人的NP问题类。计算奇偶博弈的获胜分区的最著名的确定性算法具有相对于博弈图的大小为多项式的运行时间， 但相对于博弈的指数是指数的[10]。定理6.4指标为d的二元对策G=（V;V0;E1）的获胜部分可以在空间O（djE 1）和时间O d jEjjV jbd=2cbd=2c：对等博弈的展开。设G =（V; V0; E;）是一个奇偶对策.我们假设在的范围内的最小优先级是偶数，并且具有最小优先级的每个节点v具有唯一的后继者s（v）（即，vE = fs（v）g）。这不失一般性。我们总是可以以这样一种方式转换奇偶博弈，即所有具有非最大优先级的节点都有唯一的后继者（即，仅在最不相关的节点处进行选择）。如果博弈中的最小优先级是奇数，我们考虑的是双重博弈（玩家角色互换，优先级减一）。设T是具有最小优先级的节点的集合，设G是从G中删除所有边（v; s（v））2 T得到的对策使T中的节点成为终端位置。我们将G的展开定义为一系列博弈G（其中序数上的范围），它们都与G一致，直到终端位置v 2 T的获胜条件。对于每一个，0 1i我们宣布，对于博弈G，参与人i是赢家2。此外，对于每，我们把参与人i在博弈G中的获胜集记为W。 注意W当然取决于分解T = T[ T(also关于i0 1T外的位置）。 反过来，T的分解为+ 1取决于获胜者将W置于G。 我们设定T0：= T0 0T：=\T对于极限序数：[2]从技术上讲，这意味着在G中，v是V1i中的一个位置，因此参与人i的对手必须从v移动，但不能，因此输了。301我00000111增加：W0W1WW+1W0W1W1V）的基数y，其中W=W+1=：W1 且W=W+1=：W1。WeF.这样的戏永远离不开W。如果v i2W nT，则v i+12 W因为f是G的获胜策略;如果vi2W\T=W+1\T，则v i2 T +1，这意味着，通过T +1的定义，v i+1= s（v i）2 W。但11根据定义，V =W[W对于所有 随着越来越多，01参与人0的获胜集是递减的，参与人1的获胜集是0 0 0 0 1 1 1W+1因此，存在一个序数（其基数由0 0 0 1 1 1声称这些固定点与获胜集W0和W1重合，原创游戏G引理6.5（展开引理）W=W1W = W 1。0011证据这就需要为博弈G中的参与人0和参与人1分别设计一个策略f和一个策略g，通过这个策略，参与人i在所有位置v2W1上都获胜.首先确定参与人0在G中的获胜策略f，获胜集W =W1。 注意，f平凡地扩展为博弈G的策略f，因为T中的节点在G中有唯一的后继者。 我们认为f实际上是G中从所有位置v2W获 胜 的 策 略 .要看到这一点，考虑G中从位置v02W开始的任何一局v0v1v2：，0 0 00 00 0 0一个永远不会离开W的策略必然是参与人0获胜：要么它继续，只在T中的位置上出现，然后从某个点开始，它与G中的获胜策略一致，或者它在T中的位置上出现，在这种情况下，参与人0获胜，因为在晚上被击中的最小优先级通常是偶数。为了构造博弈G中参与人1的获胜策略，我们对每个节点v2W1定义一个序数（v）：= minf：v2Wg：对于每个序数，确定参与人1的获胜策略g，在博弈G中获胜集合W，g（ v）：= g（v）（ v）对于所有 v2V1n T和g（v）：=s（v），其中v2V1\T.考虑G中从位置v02W1对g的任何博弈v0v1v2：. 我们主张只要vi2W，则1(1)vi+12W，1（二）（vi+1）（vi），以及(3)如果v是2T，则（vi+1）（vi）。<如果V2W1nT，（v）=，则v2W，因此（由于i1i i1参与人1根据他的获胜策略g在局部移动玩家031XX11111和（v i）=，则v i2T，=+ 1是后继序数，且v i+1 =不能离开她的对手的胜利集），vi+12W。 但如果v i2W1\Ts（v）2W（根据T的定义）。 因此，（v）< （v）。i1 1i+1i性质（1）、（2）和（3）意味着游隙保持在W 1内，并且值（v）正在减小。由于不存在无穷严格下降的序数链，对于xed，博弈最终仍在W内，T外（因为从T开始的移动会减少（v）的值）。因此，该策略最终与参与人1按照获胜策略g进行的策略一致。 因此，玩家1获胜。2最小不动点公式的博弈语义。为了确定LFP公式的评估游戏和分析模型检查的复杂性，可以方便地做出以下假设。首先，定点公式不应包含参数（其原因将在下面讨论）。第二，公式应该是否定范式，即，否定只适用于原子，第三，它应该是良好的命名，即， 每个定点变量仅被绑定一次，并且自由二阶变量与定点变量不同。我们将唯一子公式的D（T）写成形式[fpTx ：'（T;x）]（其中fp表示lfp或gfp）。由于技术原因，一般假设每个定点变量T只出现在D（T）中，数量的范围。这是一个常见的假设，并不影响表达能力。我们说T0依赖于T，如果T在D（T0）中自由出现.这个依赖关系的传递闭包称为依赖顺序，用@表示。T的交替水平al（T）是从T开始的@ -路上的最小和最大定点变量之间的最大交替次数。 定点句的交替深度ad（）是定点变量的最大交替水平。现在考虑一个结构A和一个LFP-公式（x），我们假设它是好的命名的，在否定范式中，并且没有参数。模型检验博弈G（A;（a））是一个等价博弈。与一阶逻辑的情况一样，博弈的位置是表达式（b），即，的子形式由A的元素实例化。初始位置为（a）。除了与定点公式和定点原子相关的位置之外，移动与一阶博弈中的移动相同。 在这样的位置有一个独特的移动（法尔西尔说）的公式定义固定点。对于一个更正式的定义，请记住，有一个很好的名字，对于任何一个固定点，变量T在[fpT：'（T;x）]（y）中是唯一的。从位置[fPTx：'（T;x）]（b）F也移动到'（T;b），并且从一个稠合的p原子Tc移动到位置'（T;c）.因此，在我们没有固定点的情况下，游戏是一阶逻辑的常见Hintikka游戏。接下来，我们考虑一个公式的情况下，只有一个出现的一个不动点算子，这是一个lfp。的在学费是从位置[lfpT：'（T;x）]（b）韦里埃试图建立在某个阶段进入T的 定点归纳法，32你是A 博弈进行到'（T;b），从那里开始，因为'是穆拉的第一阶，韦里埃要么在一个步骤的nitenmber中赢得'-博弈，要么她可以迫使它到一个位置Tc，在那里c在某个阶段进入固定点<. 然后游戏在位置（c）处恢复。作为一个ny递减序列如果序数是nite，那么Veri er将在nite步数内赢得比赛。如果公式不正确，那么法尔西尔可以在一个nite步骤中获胜，或者迫使比赛在形式Tc的许多位置上进行。因此，这些位置应该被分配优先级1（以及所有其他位置更高的优先级），以便这样的游戏将由Falsi er赢得对于gfp公式，情况正好相反。Verier想强制一个nite play，经常通过位置Tc进入，所以gfp原子被分配优先级0.在一般情况下，我们有一个公式嵌套的最小和最大在G（A;（a））的有限平面上，固定点变量通常是。但是这些变量中的一个是相对于依赖顺序@最小的。 可以证明，Aj =i这个最小的变量是gfp变量（假设玩家最优地玩）。因此，优先级标记应该为gfp-原子分配偶数优先级，为lfp-原子分配奇数优先级进一步地，如果T@T0和T;T0是不同类型的定点变量，那么T-原子的优先级应该比T0-原子低由于奇偶对策的指数是计算获胜集困难的主要来源，因此为了实现这一点，我们调整了交替级别和交替深度的定义，如果al（T）是偶数（奇数）并且T是lfp变量（gfp变量），则设置al（T）：= al（T）+ 1在其他情况下，al（T）= al（T）。最后设ad（）是中的定点变量的ad（T）的最大值。G（Ai）的位置的先验标记则由y（Ai）=al（T），如果'=T，否则。T是一个定点变量， （';）= ad（）这就完成了博弈G（A;（a））的定义。 注意，优先级标记满足上面解释的性质，并且G（A;（a））的指数至多为ad（a ） +1。定理6.6设（x）是一个取反范式的无参数LFP公式，A是一个关系结构。Aj=（a）当且仅当参与人0对博弈G（Aj（a））有获胜策略。证 据 这 是 通 过 归 纳 法 证 明 的 。 有趣的 情 况 涉 及 mula （ x ） ：=[gfpTx：'（x）]（x）的xed p 〇 i n t。在博弈G（A;（a））中，最小优先级的位置是固定