Efficient Counterexample Generation in NuSMV for Solving Push-Push Game

摘要

This paper solves Push-Push game with the model checker NuSMV which exhaustively explores all search space to determine whether a model satisfies a property. In case a model doesn't satisfy properties to be checked, NuSMV generates a counterexample which tells where this unsatisfaction occurs. However, the algorithm for generating counterexample in NuSMV traverses a search space twice so that it is inefficient for solving the game we consider here. To save the time to be required to complete the game, we modify the part of counterexample generation so that it traverses a search space once. As a result, we obtain 62% time improvement and 11% space improvement in solving the game with modified NuSMV.