Solving Sum and Product Riddle via BDD-Based Model Checking
Xiangyu Luo, Kaile Su, Abdul Rahman Sattar, Yan Chen · 2008
We model the sum and product riddle in public announcement logic, which is interpreted on an epistemic Kripke model. The model is symbolically represented as a finite state program with n agents. A model checking method to the riddle is developed by using the BDD-based symbolic model checking algorithm for logic of knowledge we developed in [7]. The method is implemented by extending the model checker MCTK [7] and then the solution of the riddle is verified successfully.