1 绪论
1.1 研究背景与现状
现今，随着互联网+、智慧城市等概念的提出，软件系统已经成为人们生活中不可或缺的组成部分，越来越多的软件为用户提供着重要的服务。然而，软件系统的泛滥会出现软件质量不可靠的现象。小型服务类软件出错可能会影响用户的使用，泄露用户隐私，给系统用户带来不便，而大型信息系统出现问题会造成用户财产损失甚至危及生命。因此，软件系统的安全性与可靠性受到越来越多的关注，而如何开发安全、可靠的软件系统成为一道难题。形式化方法是有效提高系统安全性的方法，研究形式化方法相关技术，建立软件形式化验证技术体系以提高硬件和软件系统的安全性，是非常必要的。形式化方法[1]的基本概念是通过数学方法来探究计算机科学中的相关问题，而在软件系统开发方面，形式化方法是基于数学理论来刻画系统性质的方法技术。从广义角度来讲，形式化方法是软件开发过程中分析、设计及实现的系统工程方法；狭义而言，形式化方法是软件规约和验证的方法。形式化方法又分为形式化规约方法和形式化验证方法。形式化规约是通过具有明确数学定义的文法和语义的方法或语言，对软件的期望特性或者行为进行的精确描述；形式化验证是基于已建立的形式化规格，对软件的相关特性进行数学分析和证明。模型检测（Model Checking）[2][3]是一种用于自动化验证有限状态并发系统的技术，在 20 世纪 80 年代初由美国的 Edmund M.Clarke、Allen Emerson 与法国的 Joseph Sifakis 等人分别独立提出，属于形式化验证的技术范畴。模型检测的思想是通过基于穷举搜索状态空间的方法来判断一个给定的系统模型是否满足某些预期的性质。其中，系统性质通常用时序逻辑来表示[4]，时序逻辑用于描述有限并发系统中的状态变迁序列，通过语义来隐式地表达时间，如最终一些指定的状态可以到达，或者永远不能到达一个错误状态。常用的时序逻辑包括线性时序逻辑和计算树逻辑，可以刻画有限并发反应系统的系统属性。
..........
1.2 本文主要内容及意义
博弈游戏的必胜策略验证是博弈论中研究的一个主要问题。本文首先研究了交互时序逻辑 ATL 在博弈游戏验证中的应用。在有多个参与者的系统中，ATL可以用于描述若干个参与者合作所能满足或不能满足的性质。本文用基于CUDD包实现的 ATL 符号模型检测算法对经典井字棋游戏进行了必胜策略验证。在博弈游戏的模型检测中，模型检测的规模受到博弈游戏状态空间的制约。因此，如何扩大博弈验证的规模，提升博弈验证的效率是需要研究的问题。本文提出了基于模型检测对称技术的博弈模型约简方法，根据博弈游戏的重复特性约简博弈模型的状态空间，以达到扩大检测规模、提升检测效率的目的。AlphaGo 能够以高概率赢棋，但是却不能保证在特定的情况下输棋。本课题组前期在 NSFC（U1204608）的支持下，在围棋问题中引入模型检测技术，从而在一定范围内实施穷举搜索。但是，围棋模型检测的关键在于状态空间，对围棋进行状态空间约简是需要研究的问题。本文用对称约简方法对围棋的博弈模型进行了约简，并在小棋盘上用符号模型检测方法进行了必胜策略验证与分析。本文主要进行了以上的研究，进一步完善了模型检测在博弈验证中应用。
.........
2 背景知识
2.1 模型检测
模型检测是一种自动化检测有限状态系统是否满足预期性质的形式化方法，因此模型检测需要满足形式化验证的三个基本要素：待验证系统的数学模型、描述系统性质的形式化语言和判断系统模型是否满足性质公式的检测方法[25]。在模型检测中，用有限状态迁移系统为待验证系统建立数学模型，用时序逻辑公式描述系统要满足的性质，用基于穷尽搜索的模型检测算法来判断系统模型是否满足逻辑公式。在资源足够的条件下，模型检测算法能够自动化地运行，对系统是否满足预期性质给出结果。
2.1.1 模型检测的过程
使用模型检测技术来对系统设计验证的过程包含以下 3 个步骤：1．建模 建模将系统设计转化为一个能被模型检测工具识别的系统模型。大多数情况下，这个步骤是个简单的编译过程，但是有时候由于验证时间和计算机内存的限制，设计的模型可能需要通过抽象技术来约简不相关或者不重要的细节。2．刻画 在使用模型检测工具验证之前，需要声明系统设计所需要验证的性质。性质通常采用一些逻辑语言来描述，在硬件和软件系统的验证方面，模型检测工具通常采用时序逻辑，因为这种逻辑体系能够表示系统行为随时间与状态的变化。性质描述过程中需要满足完备性，即逻辑语言能否确切表达系统所需要验证的所有性质。3．验证 使用模型检测算法来判断系统模型是否满足刻画的系统规范，如果逻辑公式不能够得到满足，算法将给出反例，指出系统不满足规范的错误轨迹。错误轨迹可以帮助设计者跟踪错误发生的具体位置，从而改正系统设计，重新进行模型检测验证，直至验证通过。
...........
2.2 符号化模型检测
显式模型检测算法通过有向图表示系统行为，用图搜索算法来计算符合系统性质的状态集合，然而随着系统规模的扩增，Kripke 结构的状态空间会呈指数级增长，因而产生状态空间爆炸的问题。符号化模型检测技术采用布尔函数表示状态集合和迁移关系，采用 OBDD 来实现布尔函数，从而利用 OBDD 操作的高效性来有效地提高了模型检测算法的效率[28][29]。符号化模型检测可以有效地缓解模型检测中的状态空间爆炸问题，目前已经被广泛采用。二元决策树不能简洁地表示布尔函数，从图 2.2 中可以看出，决策树与真值表表述布尔函数的规模基本一致。但是这种树形结构中存在着大量的冗余节点，通过合并同构子树可以得到一个能够更简洁地表示布尔公式的有根无环图，即二元决策图（Binary Decision Diagram，BDD）。Bryant[30]提出在二元决策图中增加两条约束使其遵循标准的形式，第一条约束是在从根节点出发到终端节点的路径上所有变量的出现应遵循同一变量顺序，第二条约束规定图中不存在同构子树和冗余节点。
............
3 基于 ATL 的博弈模型检测...........21
3.1 交互时序逻辑 ATL...... 21
3.1.1 交互时序逻辑介绍....21
3.1.2 ATL 符号化模型检测算法.........23
3.2 ATL 模型检测算法实现...... 25
3.2.1 CUDD....25
3.2.2 系统模型的表示........26
3.2.3 ATL 公式的表示.........27
3.2.4 算法实现验证与分析........28
3.3 井字棋模型检测......... 30
3.4 本章小结..... 32
4 基于对称的博弈模型约简...........33
4.1 对称约简算法..... 33
4.2 围棋的博弈模型......... 35
4.2.1 围棋状态自动机........35
4.2.2 围棋必胜策略描述与检测原理........38
4.3 围棋自动机的约简..... 39
4.3.1 Zobrist 哈希.....39
4.3.2 围棋的对称关系........40
4.4 实验与分析......... 42
4.5 本章小结..... 44
5 总结与展望...........45
5.1 总结..... 45
5.2 展望..... 45
4 基于对称的博弈模型约简
4.1 对称约简算法
在有限状态并发系统中，经常会出现大量的重复特征，如存储器、网络协议等等，任何带有重复特性的结构中都存在有对称性。如果能够根据系统的对称性对系统模型进行约简处理，那么这种方法既可以保留系统模型本身的性质，又能够大幅削减原始模型的规模。在围棋中，当某方落子后，棋盘上没有气的棋串会被从棋盘上提掉，这个过程称为提子。为了方便计算机处理，这里使用“伪气”来计算棋串的气。伪气是指棋盘中的每一个空的交叉点都会为周围的每个棋子提供一口气，无论四围的棋子是否属于一个棋串。如图 4.3 所示，左图中 C 和 D 两个空交叉点分别为黑子 A 和 B 各提供一口气，这时 A、B 两处黑子的伪气和气均为两口；当黑方在 C 处落子后，A、B、C 三个棋子构成一个棋串，该棋串实际上只有一口气，但是按照伪气的计算方式，空交叉点 D 为 A 和 B 各提供了一口伪气，因此棋串ACB 仍有两口伪气；当白方在 D 处落子时，空交叉点不存在，因此棋串 ACB的伪气和气都变为 0，棋串 ACB 会被从棋盘中提掉。棋盘上的棋子一旦形成棋串就不能再被分割，棋串中棋子的气共享，整串棋子要么共同存活，要么被对手提掉。基于围棋的这个特性，围棋中棋串可以使用并查集来处理。并查集是一种树型的数据结构，能够非常高效地处理不相交集合的合并与查询操作。在围棋对弈的过程中，棋子相连构成一个棋串的过程非常常见，因此使用并查集可以有效地处理棋串的合并与棋串的气的查询操作。图 4.2 中 A、B 两个黑子分别属于不同两个集合，当黑方在 C 处落子时，将A、B 两个集合并入集合 C 中构成新的集合，代表棋串 ACB，同时计算集合合并之后的伪气即可完成提子操作的处理。
..........
总结
模型检测是一种自动化的形式化验证方法，该方法将待验证的系统抽象成为形式化模型，将待验证的系统性质用时序逻辑公式描述，最后用模型检测算法来判断模型是否满足预期的性质。在交互时序逻辑 ATL 的支持下，时序逻辑公式可以用来描述开放型系统的性质，因此模型检测可以应用于对弈的验证。本文首先研究了交互时序逻辑 ATL 在博弈游戏必胜策略验证中的应用。通过交互式有穷状态自动机描述系统模型，通过 ATL 公式描述博弈游戏的必胜策略，然后用高效的符号模型检测算法进行了博弈模型的验证。本文以 CUDD 为基础实现了 ATL 符号化模型检测算法，并在经典博弈游戏井字棋进行了实验。实验得出井字棋中不存在必胜策略，这与其他方法验证结果一致，说明 ATL 符号化模型检测可以应用于博弈游戏的必胜策略验证。模型检测的关键在于状态空间，对状态空间约简是提高检测能力的有效方法。本文研究了模型检测中的对称技术，提出了基于对称技术的博弈模型约简算法。由于博弈有很高程度的对称性，对博弈模型的状态空间进行约简可以达到扩大检测规模，提高检测效率的目的。本文通过 Zobrist 哈希算法对棋盘局面编码，从而对围棋状态自动机进行了约简，在小棋盘上进行了必胜策略验证。实验说明，对称方法可以有效地对博弈模型进行约简，而且在小棋盘中用模型检测进行必胜策略验证是有效可行的。
..........
参考文献（略）