Symbolic Model Checking Epistemic Riddles By Extending ?-calculus

Dynamic epistemic logic(DEL)is used to study the change of epistemic state of agents within a multi-agent system(MAS).It is able to reason about not only the static epistemic properties of agents in a MAS,but also the dynamic epistemic properties of agents in a MAS having epistemic update actions.DEL had already been applied to the reasoning and verification of many MASs including solving epistemic riddles,epistemic programming,security communication protocols and game theory.To solving and verifying some epistemic riddles having epistemic public announcements,in this paper we propose an OBDD-based symbolic model checking method for an extension of ?-calculus with epistemic operator.A prototype of our method is implemented and is successfully applied to modeling,solving and verification of two typical epistemic riddles among philosophic community.The experimental results show that out model checking method has high performance.The main contributions of our work are summarized as follows: We first design a modelling description language to depict the epistemic riddles with a sequence of epistemic public announcements;Propose a new epistemic public announcement model with both state transition relation and agent epistemic accessibility relation;Design and implement a model construction algorithm,by which the epistemic public announcement model can be automatically generated from a modelling description program;We propose a new epistemic ?-calculus,which is an extension of ?-calculus with epistemic operator,andpresentits formal semantics over epistemic public announcement models;We design and implement an OBDD-based symbolic model checking algorithm for epistemic ?-calculus,by which we successfully model,solve and verify related temporal epistemic properties for two classical epistemic riddles: muddy children,sum and product.Our workmelds the modelling and verification method for ?-calculus,static epistemic logic and public announcement logic(a kind of dynamic epistemic logics).The temporal expressive power of the proposed epistemic ?-calculus is stronger than the existing temporal epistemic model checkers,such as MCK,MCMAS and MCTK.The well-known model checker DEMO for dynamic epistemic logics does not possess temporal reasoning ability,not to mention the temporal expression power of the proposed epistemic ?-calculus.The experimental results for the two epistemic riddles show that,our method performs exponentially better than the method based on DEMO.