Applying Model Checking Techniques to Game Solving

  • Gihwon Kwon
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3026)


In this paper, we automatically solve Push-Push game with model checking techniques which exhaustively explores all search space. Although model checking finds out the best solution for the game, it always suffers from the state explosion problem. To overcome this well-known problem, we use clever methods such as abstraction and pruning. In addition, we propose the relay model checking which decomposes the whole problem into a series of smaller one and then conquers one by one at a time. As a result, we solved all 50 levels of the game. Our solution shows better performance than human experts; that is, we solved the game with on average 22 fewer steps than human experts.


Model checking game solving state explosion problem counter-example 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  2. 2.
    Hojati, R., Brayton, R.K., Kurshan, R.P.: BDD-based Debugging of Designs using Language Containment and Fair CTL. In: Proceedings of Computer Aided Verification (1993)Google Scholar
  3. 3.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Proceedings of Computer Aided Verification, pp. 154–169 (2000)Google Scholar
  4. 4.
    Ammann, P.E., Black, P.E., Majurski, W.: Using Model Checking to Generate Tests from Specifications. In: Proceedings of ICFEM 1998, pp. 46–54 (1998)Google Scholar
  5. 5.
    Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient Generation of Counterexamples and Witness in Symbolic Model Checking. In: Proceedings of Design Automation Conference, pp. 427–432 (1995)Google Scholar
  6. 6.
    Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like Counterexamples in Model Checking. In: Proceedings of Logic In Computer Science (2002)Google Scholar
  7. 7.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) the Handbook of Theoretical Computer Science: Formal Models and Semantics, pp. 995–1072. Elsevier, Amsterdam (1990)Google Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the State Explosion Problem in Model Checking. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 154–169. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)zbMATHGoogle Scholar
  10. 10.
    Lu, Y.: Automatic Abstraction in Model Checking, Ph.D. thesis, Carnegie Mellon University,Department of Electrical and Computer Engineering (2000)Google Scholar
  11. 11.
    Chan, W.: Symbolic Model Checking for Large Software Specifications, Ph.D. thesis, University of Washington, Computer Science and Engineering (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Gihwon Kwon
    • 1
  1. 1.Department of Computer ScienceKyonggi UniversitySuwon-Si, Kyonggi-DoKorea

Personalised recommendations