G. Kwon (Korea)
Model checking, State space explosion, Optimization,Abstraction, Pruning
This paper presents our experiences on automatically solving the SokoMind PLUS game with the model checker SMV. The state space of the game is represented as a finite state model. But its state space is so huge that it couldn't handle it directly with SMV. Thus optimizations are crucial for successful solving the game with SMV. This paper uses two optimizations such as abstraction and pruning. As a result, we have two world records in Level 13 and 15 of the game.
Important Links:
Go Back
