The Research And Application Of Symbolic Model Checking

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.