《对弈必胜策略的符号化模型检测》由会员分享，可在线阅读，更多相关《对弈必胜策略的符号化模型检测（3页珍藏版）》请在金锄头文库上搜索。
1、计算机科学2 0 0 6 V 0 1 3 3 N Q 8 ( 增刊)对弈必胜策略的符号化模型检测S y m b o l i cM o d e lC h e c k i n gW i n n i n gS t r a t e g i e si nG a m e s何青1 - 2 骆翔宇1 3 苏开乐1( 中山大学计算机科学系广州5 1 0 2 7 5 ) 1( 湖南文理学院计算机科学系常德4 1 5 0 0 0 ) 2( 暨南大学计算机科学系广州5 1 0 6 3 2 ) 3A b s t r a c tI nt h et w o - p l a y e rz e r o - s u mg a
2、m e s ，v e r i f y i n gw h e t h e rt h e r ee x i s t sw i n n i n gs t r a t e g i e sh a sn o tb e e ns o l v e dp r o p e r l y ，s i n c ei tr e f e r st ot h ee x h a u s ts e a r c h e so ft h ef i n i t es t a t es p a c e W i t ht h ed e v e l o p m e n to fs y m b o l i cm o d e lc h e c k
3、 i n g ，h o w e v e r ，v e r i f y i n gl a r g es y s t e m sb e c o m e sp o s s i b l BI nt h i sp a p e r ，w ep r e s e n tac o n f l l - T l o nm e t h o df o rv e r i f y i n gt h ew i n n i n gs t r a t e g i e so fg a m e sw i t hs y m b o l i cm o d e lc h e c k i n g ，a n dg i v eac a s es
4、 t u d yf o rT i c - T a c - T o eu s i n go u rm o d e lc h e c k e rM C T KK e y w o r d sS y m b o l i cm o d e lc h e c k i n g ，B D D s ，Z e r o - s u mg a m e s ，W i n n i n gs t r a t e g y1引言在对弈问题的研究中，人们一直都在探询这样的问题：对弈中的某一方是否存在必胜策略，也就是说无论对手如何行棋，该方是否总是能够战胜对手。从搜索技术的角度来看，这将需要对棋局的状态空间进行穷举搜索，因此启发式
5、搜索技术无法很好地解决这个问题。然而从形式化方法的角度来看，这个问题可归结为棋局模型中的形式化验证问题，即模型检测( M o d e lC h e c k i n g ) c 1 4 问题。而符号化模型检测( S y m b o l i cM o d e lC h e c k i n g ) 1 3 技术的出现和发展给我们提供了研究必胜策略的新途径。符号化模型检测技术自上个世纪9 0 年代出现以来已经普遍应用于大规模集成电路系统的设计中。作为一种形式化验证技术，符号化模型检测能验证的状态规模已经达到。这种技术是对传统模型检测技术的巨大改进，它通过使用二值判定图( B D D s ) 5 这种高
6、效的数据结构来建立系统模型，并将需要验证的系统性质进行形式化描述，进而在超大规模的状态空间中验证系统性质。近年来关于对弈中必胜策略的形式化研究日益增多，这一切都得益于B D D s 技术的发展，它使得遍历更大规模的状态空间成为了可能。E d e l k a m p 7 将可达性分析( R e a c h a b i l i t yA n a l y s i s ) 与B D D s 结合来验证井字棋中的必胜策略，而H u r d 8 J 则将定理证明器( T h e o r e mP r o v e r ) 与B D D s 相结合来验证国际象棋残局中的必胜策略。他们的尝试为本文的工作提供了坚
7、实的理论和实践基础。本文通过符号化模型检测技术来验证井字棋中是否存在必胜策略，实验工具是我们开发的符号化模型检测工具M C T K ，它是基于文 1 ，3 的理论而开发的。它不仅能验证系统的时态性质，而且还能对系统的知识性质进行验证。本文的结构如下：第2 节简要介绍符号化模型检测的基础知识；第3 节给出使用符号化模型检测来验证必胜策略的一般方法；第4 节以井字为例实现这种方法并给出相关的实验结果；最后对我们的工作做出总结并提出今后的研究方向。2 符号化模型检测模型检测是一种形式化验证技术，它能在一个有限状态系统模型中验证系统的某些性质。系统模型是一个克里普克结构M = ( S ，R ，L )
8、，其中S 是一个有限状态集合，R 是S 上的状态迁移关系且有R S xS ，而L 则是一个标记函数LlS - + P ( a t o m ) ，它将状态集合S 中的每个状态映射到一个原子命题集合的幂集上。系统的性质可以被描述为时态逻辑公式1 5 ，主要分为计算树逻辑( C T I 。) 公式和线性时态逻辑( I 。T I 。) 公式。在给定的初始状态j 下，模型检测实质上就是要验证M ， j 5 是否为真。传统的模型检测技术可验证的状态空间 分有限，而且往往伴随着状态爆炸的问题，即随着系统复杂度的增加，系统的状态数量成指数增长，这就给系统验证带来了极大的麻烦。而符号化模型检测是基于二值判定图来
9、进行模型检测的，它很好地解决了状态爆炸的问题。下面首先来介绍一下二值判定图的知何青硕L 研究生研究方向：模捌榆测，知识推理等。骆翔宇博L 研究生，研究方向：模型检测、知识推理，安全协 义验证等。苏开乐教授，博1 生导师研究方向：模到榆测、知识推理、安全协议验证等。2 6 6 识。2 1 二值判定图二值判定图( B i n a r yD e c i s i o nd i a g r a m s ) 是一种表示布尔函数的高效方法，它首先是作为一种简单的形式，即二值判定树( B i n a r yD e c i s i o nT r e e s ) 被提出来的。二值判定图中每一个非终端结点用布尔变量
10、z ，Y ，z 标记，终端结点用1 或0 标记。每一个非终端结点u 由一个变量v a r ( v ) 标识，它有两个后继结点：l o w ( v ) 对应着变量口被赋值成为0 的情况，h i g h ( v ) 对应着变量可被赋值为1 的情况。而每一个终端结点V 被表示为v a l u e ( v ) ，v a l u e ( v ) 要么是0要么是1 。从初始结点出发到终端结点，我们可以确定该路径上对变量的真值赋值是否使该二值判定图表示的布尔公式为真。判断方法为：如果变量口被赋值为0 ，那么从根结点到终端结点的路径上的下一个结点将是l o w ( v ) ；如果V 被赋值为1 ，那么路径上的
11、下一个结点将是h i g h ( v ) 。2 2p 演算符号化模型检测主要用来验证包括计算树逻辑 ( C T L ) 和线性时态逻辑( L T L ) 的时态逻辑公式。计算树逻辑是一种有名的分支时间逻辑，其时态算子由路径算子和状态算子所组成。它主要用于符号 化模型检测工具S M V 和N u S M V 中。在很多情况下，时态逻辑公式的验证问题要涉及到不动点的运算。肛演算( 肛一C a l c u l u s ) 是在计算树逻辑的分支时间语法中加入了最大和最小不动 点。对于变量z 和命题公式厂，肛，和船f 分别表示厂对于变量z 的最小不动点和最大不动点。3 必胜策略的形式化验证方法3 1 描
12、述棋局模型我们称棋局的每一个局面为一个棋局状态，所有棋局状态的集合可记为S 。若是在某个状态s f fS下，行棋的一方能按照规则使棋局达到另一个状态s 7 ，则称( s ，5 7 ) 为一个状态迁移关系。我们将S 上所有的状态迁移关系记为R ，其中R 互S S 。首先来描述棋局全局状态的集合S 。我们可以定义一个布尔变量的集合口一 z 。，z 2 ，z 。) ，然后 通过标记函数L ：p P ( u ) 来对S 进行编码( P ( u )表示铷的幂集) 。对于某个状态s S ，我们可以通过布尔函数六一z 1 z z Z ，。来表示，其中若是五L ( s ) ，贝0 厶为z i ，否贝0Z f
13、为X ，。接下来描述状态迁移关系R 。由于状态迁移关系R 至S S ，我们还需要一份变量的拷贝，其可表示为V 7 = z 7 1 ，z7 2 ，z7 ，。 。对于某迁移关系( S ，s 7 ) R ，我们可以用布尔函数厂( ，) 一( Z l Z 2 z 。)( Z 7 1 ，7 2 ，7 。) 来表示，其中若z ，L ( s ) ，则，为z ，否则Z 。为；，；若r 7 ，L ( s 7 ) ，则，7 ，为丁7 ，否则z 7 ；为；7 i 。于是，全局迁移关系R 可以通过将所有( r ，) R 的布尔函数厂( ) 用“+ ”算符进行运算而得到。3 2 描述必胜策略对弈中某方的必胜策略实质是对
14、该方所有的获 胜状态的集合进行不动点运算，B a c k h o u s e 以及M i c h a e l i s 6 对此进行了详尽的论证。因此我们便可以用p 演算公式来描述对弈双方的必胜策略。假 设对弈双方分别为P 1 和P 2 ，定义布尔变量P 1 -m o v e 、P 2 一m o v e 分别表示当前为P l 和P 2 行棋，布尔函数如一曲、如一嘲分别表示P 1 和P 2 的所有获 胜状态的集合，则P 1 和P 2 必胜的肛演算公式分别为：虾l 一。籼：一# z z ( P l 一。V ( P 1 一m o v eAE X x ) V ( P 2 _ m o v eAA X x
15、) ) ，如一。晌：一肛( 如一曲V ( P 2 一m o v e A E X x ) V( P 1 一m o v eAA X x ) ) ( 若厂是一个C T L 公式，则C T I 。公式A X f 表示，在所有下一步状态都成立；C T I 。公式E X f 表示在所有下一步状态中，至少有一个状态使得，成立。)3 3 形式化验证必胜策略完成了对棋局模型和必胜策略的形式化描述之后，我们只需要在棋局模型和给定的初始状态下来 验证必胜策略是否可满足。假设棋局的模型为M ，棋局的初始状态为J ，我们只需要分别来验证M ，J = 蛔。肭和M ，j 蝻一一。的结果是否为真：如果 前者为真则说明P 1
16、总是能找到获胜的策略，后者为真则说明P 2 总是能找到获胜的策略，而两者都不为真则说明双方都不能确保必然获胜。下面给出验证必胜策略的算法，用伪代码表示：算法1对弈必胜策略的验证算法P r o c e d u r eC h e e k W i n ( s i d e ，i n i t ，w i l Ls t a t e s ) b e g i n B D Dt e m p l ，t e m p 2 ，t e m p 3 ，i s w i n ； B D DS t a t e s - - s e t ：= C h e e k S A T ( w i n _ s t a t e s ) ； w h i l e ( t r u e )b e g i n t e m p l ：= B D D - A n d ( s i d e ，C h e c k E X ( s t a t e s - s e t ) )
