Efficient Counterexample Generation for Game Solving in NuSMV


The KIPS Transactions:PartD, Vol. 10, No. 5, pp. 813-820, Aug. 2003
10.3745/KIPSTD.2003.10.5.813,   PDF Download:

Abstract

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 revise 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.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from September 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
K. G. Hyeon and L. T. Hun, "Efficient Counterexample Generation for Game Solving in NuSMV," The KIPS Transactions:PartD, vol. 10, no. 5, pp. 813-820, 2003. DOI: 10.3745/KIPSTD.2003.10.5.813.

[ACM Style]
Kwon Gi Hyeon and Lee Tae Hun. 2003. Efficient Counterexample Generation for Game Solving in NuSMV. The KIPS Transactions:PartD, 10, 5, (2003), 813-820. DOI: 10.3745/KIPSTD.2003.10.5.813.