A complete coalition logic of temporal knowledge for multi-agent systems  

作　　者：Qingliang CHEN Kaile SU Yong HU Guiwu HU 

机构地区：[1]Department of Computer Science, Jinan University, Guangzhou 510632, China [2]Institute for Integrated and Intelligent Systems, Griffith University, Brisbane Qld 4111, Australia [3]3 Institute of Business Intelligence and Knowledge Discovery,Guangdong University of Foreign Studies, Guangzhou 510006, China [4]School of Mathematics and Statistics,Guangdong University of Finance and Economics, Guangzhou 510320, China

出　　处：《Frontiers of Computer Science》2015年第1期75-86,共12页中国计算机科学前沿（英文版）

基　　金：This work was supported by National Basic Research Program of China （973 Program） （2010CB328103）; the National Natural Science Foundation of China （Grant Nos. 61272415, 61003056, 71271061 and 61370177）; ARC Future Fellowship （FT0991785） and Business Intelligence Key Team of Guangdong University of Foreign Studies （TD 1202）.

摘　　要：Coalition logic （CL） is one of the most influential logical formalisms for strategic abilities of multi-agent systems. CL can specify what a group of agents can achieve through choices of their actions, denoted by [C]φ to state that a group of agents C can have a strategy to bring about φ by collective actions, no matter what the other agents do. However, CL lacks the temporal dimension and thus can not capture the dynamic aspects of a system. Therefore, CL can not formalize the evolvement of rational mental attitudes of the agents such as knowledge, which has been shown to be very useful in specifications and verifications of distributed systems, and has received substantial amount of studies. In this paper, we introduce coalition logic of temporal knowledge （CLTK）, by incorporating a temporal logic of knowledge （Halpern and Vardi＇s logic of CKLn） into CL to equip CL with the power to formalize how agents＇ knowledge （individual or group knowledge） evolves over the time by coalitional forces and the temporal properties of strategic abilities as well. Furthermore, we provide an axiomatic system for CLTK and prove that it is sound and complete, along with the complexity of the satisfiability problem which is shown to be EXPTIME-complete.Coalition logic （CL） is one of the most influential logical formalisms for strategic abilities of multi-agent systems. CL can specify what a group of agents can achieve through choices of their actions, denoted by [C]φ to state that a group of agents C can have a strategy to bring about φ by collective actions, no matter what the other agents do. However, CL lacks the temporal dimension and thus can not capture the dynamic aspects of a system. Therefore, CL can not formalize the evolvement of rational mental attitudes of the agents such as knowledge, which has been shown to be very useful in specifications and verifications of distributed systems, and has received substantial amount of studies. In this paper, we introduce coalition logic of temporal knowledge （CLTK）, by incorporating a temporal logic of knowledge （Halpern and Vardi＇s logic of CKLn） into CL to equip CL with the power to formalize how agents＇ knowledge （individual or group knowledge） evolves over the time by coalitional forces and the temporal properties of strategic abilities as well. Furthermore, we provide an axiomatic system for CLTK and prove that it is sound and complete, along with the complexity of the satisfiability problem which is shown to be EXPTIME-complete.

关 键 词：coalition logic temporal logic of knowledge complete axiomatization multi-agent systems 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程] TP31[自动化与计算机技术—控制科学与工程]