Symbolic Model Checking Algorithm for Temporal Epistemic Logic CTL*K
时态认知逻辑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 agent...