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

Volume

3

fYear

2008

fDate

9-12 Dec. 2008

Firstpage

630

Lastpage

633

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/WIIAT.2008.277

Filename

4740858