Symbolic Model Checking Algorithm for Temporal Epistemic Logic CTL*K

Temporal epistemic logics have been gradually used in specification of multiple agents system,which are composed by temporal logics and epistemic logics.Most of temporal epistemic logics are based on CTL,which have a limited expressivity.And some model checking techniques existing for them have problems such as memory-shortage and state-explosion.A temporal epistemic logic CTL*K based on CTL* was proposed.Through the definition of syntax and semantics,CTL*K had a strong expressivity and could describe agents' epistemic properties such as belief and goal.To check CTL*K,a symbolic model checking algorithm for CTL*K was offered,which translated a CTL*K formula into a common CTL* formula and could be easily encoded into NuSMV model checker.The experiment showed that the algorithm could obviously enlarge the size of system to be checked.