%0 Journal Article
%T Symbolic Model Checking Algorithm for Temporal Epistemic Logic CTL*K<br>时态认知逻辑CTL＊K的符号化模型检查算法
%A CHEN Bin
%A WANG Zhi-xue
%A <br>陈彬
%A 王智学
%J 计算机科学
%D 2009
%I 
%X 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...
%K Symbolic model checking
%K Multiple agent system
%K Temporal epistemic logic<br>符号模型检测
%K 多主体系统
%K 时态认知逻辑
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=2290CCABA364ABAF5CD10ED6154DF0EA&yid=DE12191FBD62783C&vid=933658645952ED9F&iid=94C357A881DFC066&sid=797D49279EA93BC4&eid=D5C73DEF4CF8FAF3&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=16