【作者】 孔庆爱；

【导师】 欧阳丹彤；

【作者基本信息】 吉林大学 ， 计算机软件与理论， 2008， 硕士

【摘要】 在计算机科学中,博弈理论与逻辑的一个非常显著的应用领域是并发系统理论,本文主要围绕模型检测在博弈领域中的应用及形式化逻辑与博弈理论的内部联系展开研究,主要工作有:1.首先介绍了符号模型检测技术,包括模型检测技术的原理、过程和算法实现。因为符号模型检测的提出最初是为了解决状态爆炸问题,这里我们还介绍了几种解决状态爆炸问题的方法。2.研究了符号模型检测在博弈游戏中的应用,在符号模型检测方法的理论框架下将两个典型的博弈游戏进行形式化分析。并在符号模型检测工具NuSMV基础上进行修改,加入算法实现了博弈游戏的形式化验证。实验结果证明符号模型检测为解决博弈游戏问题提供了可行的方法。3.为了减小经典的形式化逻辑和博弈之间的差距,本文从内部进行探索,给出CTL*框架下Kripke结构基础上的2-player博弈,给出了一种博弈规则,并考察了其正确性。博弈模型检测方法的优势在于为公式及公式所表示的属性提供了直观清晰的便于理解的框架。更多还原

【Abstract】 Model checking is a formal verification technology for limited states concurrent systems. There are many advantages over simulation and theorem provers in verification. In model checking technology,it captures the behavior of reactive systems by a type of state transition graph called Kripke structure , and describes the specification by temporal logic such as computation tree logic (CTL*). The procedure of model checking is to verify whether the system satisfies the specification. In initial years, the state space was explicit expressed and model checking suffered from the state space explosion and the size of the system. Mcmillan dealt with the problem by OBDD and fixpoint theory ofμ?calculus, this method is called symbolic model checking. The advantage of symbolic model checking is that it is able to verify the system properties on the large space of states, which means, it has the ability to search on huge space of states. Recent years, model checking is not only outstanding in the verification of circuits, security protocol, and softwares, but also has played an important role in AI regions such as planning and muti-agent systems.Game theory has been one of the main areas of the artificial intelligence. In the two-player games, verifying whether there exists winning strategies has not been solved properly, since it refers to the exhaust searches of the finite states space. That is to say no matter how the opponent to move, the player is always able to win. From the point of search technology, it will require exhaustive searches of the states, so the heuristic search technology is not the good methods to solve this problem. But from the point of formal methods, the problem can be summed up a problem of formal verification in the model system. Though the theoretical complexity of solving various games in the literature is well understood, there has been relatively less effort spent in identifying how the powerful symbolic techniques used in model checking fare in solving games with large state-spaces. In formal verification, games have several applications in verifying reactive systems where the agents comprising the system are viewed as players of a game: in modular verification, in compatibility checking of formal interface for modules, in approached to compositional verification. In the paper, games have been used to solve model checking, which is called model checking games.At the beginning, we put focus on the introduction of basic knowledge of symbolic model checking, including the principles, processes, and algorithms. The main work can be summarized as two points; we first discuss its applications in games, and then explore the relation between model checking and game theory which is called model checking game.Firstly, we solved two classical games with the method of formulization under the framework of the model checking. The Tic-Tac-Toe game is modeled as a transition system. We designed a game strategy based on winning state and describe the strategy under different frameworks which provides reference methods under these frameworks, and then we gave the corresponding algorithms. And finally we solved the formalized model checking problem using a model checker. Here we solved two classical games, Tic-Tac-Toe and Nim. The two players of the former game both have no winning strategy; while one of the two players in the latter must have winning strategy. We obtain the same results as the literature about Tic-Tac-Toe games and the results is consistent with the actual analysis of Nim. Hence we have reached a conclusion that the symbolic model checking techniques offered a new and significative method for solving games. It also expounds the application areas of the symbolic model checking.Secondly,we put focus on the model checking games. Model checking games played by two players on the system and the formula provide such features. Answering the question about the property being fulfilled turns out to be equivalent to finding a winning strategy for one of the players. However, verification of traditional model checking is often combined with specification expressed properties with the temporal logic. In fact, regarding aspects of internal structure, the gap between classical formal logics and game-oriented language is very large. We address the question of relating classical formal logics and game logics with regard to their fine-structure, and try to bridge the gap between these in a specific setting concerning the CTL* based on the Kripke structure. Here, we solve model checking problem by the method of games. We defined CTL * model checking games, and we gave the rules under the framework of the game, then the conditions when a play ends and the definition of victory in the model checking games. Then we can apply these rules to play games and look for a winning strategy to answer the question about the property being fulfilled. In this paper, we cited an example and have given a detailed explanation. Finally, we showed the connectedness of the model checking games.The bottleneck of symbolic model checking is the memory space occupied by BDDs, and it’s impossible to carry on verifications directly using the techniques of symbolic model checking for the games with complex rules and large state-spaces. The regularly used min-max search is a good method in games, in which a sophisticated evaluates states. However, model checking winning state is much significative in this case because knowing which states are winning states can be helpful in evaluating the states in min-max search.In contrast to automata-theoretic approached it is not necessary to take a detour via satisfiability checking first. The main advantage of games in logics is to provide a clear understanding of formulas and the properties they express. There are various models for the concurrent system and the model checking for CTL* was an early one. As being introduced in chapter 2, CTL* subsumes other temporal logics like LTL and CTL, and thus the results on the games for CTL* easily carry over to these other logics as well.更多还原