双主体零和博弈逻辑形式系统建构及模型检测研究，本文主要内容关键词为：主体论文,逻辑论文,模型论文,形式论文,系统论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
中图分类号：B 819 文献标识码：A 文章编号：1000-260X(2011)06-0047-07
双主体零和博弈逻辑是博弈逻辑的一个重要分支，也是目前国际上博弈逻辑研究的重心。目前对双主体零和博弈逻辑的研究主要是结合动态逻辑来进行的。双主体博弈逻辑就是两个各自独立决策，但策略和利益具有相互依存关系的博弈方如何合理选择策略的逻辑。零和博弈逻辑研究的是博弈双方得益之和等于零的情况，在零和博弈中，博弈方的利益是完全相反的，没有任何调和的余地。本文在命题动态逻辑原有程序算子(；∪*)的基础上增加对偶(dual)算子d来建构双主体零和博弈逻辑的形式系统，并探究其模型检测的复杂性。
一、双主体零和博弈逻辑形式系统
1.语法和语义
双主体零和博弈逻辑的语言由博弈和命题两类构成。在双主体零和博弈中有两个博弈方(参与人)，分别为参与人1和参与人2。
在某些情况下，把参与人2的选择和迭代作为初始算子，可以让我们思考在对偶范式下的博弈逻辑公式和博弈。
定义4(对偶范式)：双主体零和博弈逻辑公式(或博弈)是对偶范式，当且仅当对偶算子仅出现在参与人2的迭代、选择中或恰好在原子博弈或测试之前。
根据德摩根律，每一个双主体零和博弈逻辑公式可以写成一个等价的对偶范式：
目前，学界仅对双主体零和博弈逻辑的弱完全性定理给出了证明。波利在他2001年的博士论文《关于社会软件的逻辑》中对不带有迭代算子*的双主体零和博弈逻辑完全性定理给出了证明[2]。但是关于有迭代算子*的双主体零和博弈逻辑GL-*对所有双主体零和博弈模型是完全的证明，仍然是一个未解决的技术问题。
二、双主体零和博弈逻辑嵌入μ-演算
1.μ-演算
我们将介绍模态μ-演算的语言，并把它的语义从克里普克模型扩展到双主体零和博弈模型。接下来，我们把双主体零和博弈逻辑的公式平移成μ-演算的公式，进而讨论双主体零和博弈逻辑的语言表达力。
定义9(正范式)：如果公式φ变元没有被约束(即被μ或ν约束)两次，并且所有在φ中出现的否定符仅应用于原子命题，则公式φ就称为是正范式。
使用布尔联结词的德摩根律，单元菱形的对偶性和极大不动点，每一个μ-演算公式都可以改写成正范式。
在讨论模型检测的算法时，不动点嵌套起着关键性的作用。最简单的一类嵌套可以用下面公式表示：
μX.p∨(X∧μY.q∨＜g＞Y)
因为变元X不出现在μY不动点的内层，后者可以不依赖于μY不动点先行计算。我们把这种嵌套看成为空嵌套。非空嵌套可以用以下公式表示：
μX.p∨(q∧μY.X∨＜g＞Y)
式中内层不动点的计算依赖于X的现行值。在忽略空嵌套的情况下，我们把μ-演算公式φ的不动点深度d(φ)定义为这种嵌套的最大数。在我们看到的这种偶数嵌套中，被嵌套的两个不动点都是最小不动点。另一方面，下面的公式则是在最小不动点的内层嵌套了一个最大不动点。
μX.p∨(q∧νY.X∨＜g＞Y)
这种嵌套在形式上是通过交换深度(alternation depth)的概念来表达的。
2.把双主体零和博弈逻辑嵌入到μ-演算中
这就证明所有双主体零和博弈逻辑公式都不能等价于交换深度ad小于2的μ-演算公式。
定理4：如果公式在双主体零和博弈逻辑的程序片断内，则ad(φ)=1，因此双主体零和博弈逻辑比它的程序片断有更强的表达力[5]。
三、双主体零和博弈逻辑模型检测的复杂性
为了对双主体零和博弈逻辑模型检测进行分
析，我们首先需要描述一个双主体零和博弈模型，并定义它的大小。
在现实生活中双主体博弈的情况非常普遍，双主体零和博弈逻辑的研究不仅是博弈逻辑理论研究的重心，而且也具有重要的应用价值。对双主体零和博弈逻辑的研究可以推动博弈逻辑研究向纵深发展，从而促进应用逻辑的繁荣。
注释：
①在数学领域序理论和格理论中，克纳斯特-塔斯基定理得名于克纳斯特(Bronis
aw Knaster)和阿尔弗雷德·塔斯基(Alfred Tarski)，它声称：设L是完全格，并设f：L→L是保序映射，则f在L中的不动点的集合也是完全格。因为完全格非空，这就保证f至少有一个不动点存在，甚至一个“最小”(或“最大”)不动点存在。在很多实际情况中，这是这个定理最重要的含义。