Symbolic Model Checking for Sum and Product Riddle
Rongsheng Dong · 2008
The Sum-and-Product Riddle is a famous number puzzle.The riddle is modeled in a modal logic called public announcement logic,which is interpreted on multi-agent Kripke model.The model is symbolically represented as a multi-agent finite state program.Based on the semantics of the logic,a symbolic model checking approach to the riddle is developed by using the symbolic model checking algorithm for logic of knowledge under the semantics of interpreted systems with local propositions.The approach is then implemented by extending the model checker NuSMV and in which the solution of the riddle is verified successfully.The riddle is also verified by using the epistemic model checker DEMO in the same experimental environment.The comparison between the experimental results from the two model checkers show that the running efficiency of our model checking approach is much higher than that of DEMO.