Title :
Solving Sum and Product Riddle via BDD-Based Model Checking
Author :
Luo, Xiangyu ; Su, Kaile ; Sattar, Abdul ; Chen, Yan
Author_Institution :
Tsinghua Nat. Lab. for Inf. Sci. & Technol. Key Lab. of Security for Inf. Syst. of Minist. of Educ. Sch. of Software, Tsinghua Univ., Beijing
Abstract :
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.
Keywords :
formal verification; knowledge engineering; multi-agent systems; BDD-based model checking; MCTK; epistemic Kripke model; finite state program; knowledge logic; multiagent system; public announcement logic; sum and product riddle; Automatic logic units; Boolean functions; Computer science; Computer security; Data structures; Educational technology; IEEE news; Information science; Intelligent agent; Laboratories; OBDD; logic of knowledge; model checking; public announcement logic;
Conference_Titel :
Web Intelligence and Intelligent Agent Technology, 2008. WI-IAT '08. IEEE/WIC/ACM International Conference on
Conference_Location :
Sydney, NSW
Print_ISBN :
978-0-7695-3496-1
DOI :
10.1109/WIIAT.2008.277
