基于ATL的博弈模型检测研究及其在围棋中的应用

发布时间：2018-05-27 14:45

本文选题：模型检测 + 交互时序逻辑　；参考：《郑州大学》2017年硕士论文

【摘要】：模型检测是由美国Clarke教授等提出的一种用于自动化验证有穷状态并发系统的技术。该技术通过穷举搜索状态空间的模型检测算法来验证系统模型是否符合预期属性。由于状态空间随着系统规模急剧增长,符号化模型检测被提出从而有效地缓解状态空间爆炸问题。验证对弈中某方是否存在必胜策略是博弈论中研究的一个主要问题。基于符号模型检测的高效性,模型检测可以应用于博弈游戏的验证。交互时序逻辑ATL对计算树逻辑进行了扩充,可以用来描述开放系统的性质。利用ATL符号模型检测算法可以对博弈游戏模型进行验证。然而,一些博弈游戏的状态空间过于庞大,需要对博弈模型检测方法进一步改进来扩大可验证系统的规模。本课题组前期在NSFC的支持下,在围棋中引入模型检测技术从而在一定范围内实施穷举搜索。然而,实施围棋模型检测的关键在于状态空间,如何约简状态空间是当前迫切需要解决的问题。针对以上的问题,本文做了一些工作如下:1)在博弈游戏的必胜策略检测验证中引入了ATL模型检测技术。用ATL对经典博弈游戏井字棋进行了建模与分析,实验结果与其他方法验证的结果一致。2)将对称技术应用于博弈模型检测中,提出了基于对称技术的博弈模型约简方法。由于很多博弈游戏具有重复的特征,对称技术可以有效地用于博弈模型的约简。3)对围棋的博弈模型进行约简,并用符号模型检测算法在小棋盘进行了必胜策略检测验证,表明了模型检测技术及其约简算法在围棋博弈中的有效性和可行性。
[Abstract]:Model checking is a technique proposed by Professor Clarke of the United States to automate the verification of finite state concurrency systems. This technique verifies whether the system model conforms to expected attributes by exhaustive search of the model checking algorithm of state space. As the state space increases rapidly with the system scale, symbolic model detection is proposed to effectively alleviate the state space explosion problem. To verify the existence of a winning strategy is a major problem in game theory. Based on the efficiency of symbolic model detection, model detection can be applied to game verification. Interactive temporal logic (ATL) extends computing tree logic to describe the properties of open systems. ATL symbol model detection algorithm can be used to verify the game model. However, the state space of some game games is too large, so it is necessary to further improve the game model detection method to expand the scale of the verifiable system. With the support of NSFC, the research group introduced model checking technology in go to carry out exhaustive search in a certain range. However, the key to implement go model detection is the state space. How to reduce the state space is an urgent problem to be solved. In order to solve the above problems, this paper does some work as follows: (1) the ATL model detection technique is introduced in the verification of the winning strategy of game games. In this paper, ATL is used to model and analyze the classical game well word chess. The experimental results are in agreement with the results of other methods. (2) the symmetry technique is applied to the game model detection, and a game model reduction method based on the symmetry technology is proposed. Because many game games have the characteristics of repetition, symmetry technique can be used to reduce the game model of go effectively, and the sign model detection algorithm is used to test the winning strategy on the small chessboard. The effectiveness and feasibility of model detection and its reduction algorithm in go game are demonstrated.
【学位授予单位】：郑州大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP317;TP311.53

【相似文献】