A Model Checking Approach for Solving Epistemic Riddles
Luo Xiang · Chinese Journal of Computers · 2010
This paper aims to model and solve the Sum and Product Riddle in public announcement logic.A dynamic epistemic model is proposed,that is the linear temporal combination of the epistemic model of environment and the epistemic models after each announcement,such that the authors' model checking technique for temporal epistemic logic can be extended to support the modeling and verification of public announcement logic.This model checking method not only can help to find all solutions,but also verify related temporal epistemic properties.Such characteristic is not fully supported by the current version of MCK,MCMAS and DEMO.The authors implemented the proposed method in the symbolic model checker MCTK via OBDD and verified the sum and product riddle.The experimental results show that the proposed method is correct and efficient.