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

Abstract

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]\varphi to state that a group of agents C can have a strategy to bring about \varphi 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 CKL_n) 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.

Keywords

coalition logic / temporal logic of knowledge / complete axiomatization / multi-agent systems

References

[1] Hoek van der W, Wooldridge M. Multi-agent systems. Handbook of Knowledge Representation. Elsevier Press, 2008, 887-928

[2] Shoham Y, Leyton-Brown K. Multi-agent Systems: Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press, 2008

[3] Wooldridge M. An Introduction to Multiagent Systems. 2nd ed. John Wiley & Sons Press, 2009

[4] Wooldridge M. Reasoning about Rational Agents. MIT Press, 2000

[5] Hoek van der W, Wooldridge M. Logics for multi-agent systems. In: Weiss G, ed. Multi-Agent Systems 2nd ed. MIT Press, 2013, 671-810

[6] Halpern J Y, Fagin R, Moses Y, Vardi M Y. Reasoning About Knowledge. MIT Press, 1995

[7] Meyer J J C, Hoek van der W. Epistemic Logic for AI and Computer Science (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press, 2004

[8] Osborne M J, Rubinstein A. A Course in Game Theory. The MIT Press, 1994

[9] Pauly M. A modal logic for coalitional power in games. Journal of Logic and Computation, 2002, 12(1): 149-166

[10] Alur R, Henzinger T A, Kupferman O. Alternating-time temporal logic. Journal of the ACM, 2002, 49(5): 672-713

[11] Broersen J. A complete STIT logic for knowledge and action, and some of its applications. Lecture Notes in Computer Science, 2009, 5397: 47-59

[12] Hoek van der W, Wooldridge M. Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications. Studia Logica, 2003, 75(1): 125-157

[13] Ågotnes T, Alechina N. Epistemic coalition logic: completeness and complexity. In: Proceedings of the 11th International Conference on Autonomous Agents and Multiagent Systems. 2012, 1099-1106

[14] Ågotnes T, Hoek van der W, Wooldridge M. Quantified coalition logic. Synthese, 2008, 165(2): 269-294

[15] Boella G, Gabbay D M, Genovese V, Torre van der L. Higher-order coalition logic. In: Proceedings of the 19th European Conference on Artificial Intelligence. 2010, 555-560

[16] Ågotnes T, Hoek van der W, Wooldridge M. Reasoning about coalitional games. Artificial Intelligence, 2009, 173(1): 45-79

[17] Troquard N, Walther D. Alternating-time dynamic logic. In: Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems. 2010, 473-480

[18] Walther D, Hoek van der W, Wooldridge M. Alternating-time temporal logic with explicit strategies. In: Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge. 2007, 269-278

[19] Seylan I, Jamroga W. Description logic for coalitions. In: Proceedings of the 8th International Joint Conference on Autonomous Agents and Multiagent Systems. 2009, 425-432

[20] Bulling N, Dix J, Chesñevar C I. Modelling coalitions: ATL+ argumentation. In: Proceedings of the 7th International Joint Conference on Autonomous Agents and Multiagent Systems. 2008, 681-688

[21] Halpern J Y, Vardi M Y. The complexity of reasoning about knowledge and time: extended abstract. In: Proceedings of the 18th Annual ACM Symposium on Theory of Computing. 1986, 304-315

[22] Goranko V, Drimmelen van G. Complete axiomatization and decidability of alternating-time temporal logic. Theoretical Computer Science, 2006, 353(1-3): 93-117

[23] Broersen J, Herzig A, Troquard N. A normal simulation of coalition logic and an epistemic extension. In: Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge. 2007, 92-101

[24] Broersen J, Herzig A, Troquard N. What groups do, can do, and know they can do: an analysis in normal modal logics. Journal of Applied Non-Classical Logics, 2009, 19(3): 261-290

[25] Rapoport A, Chammah A M. Prisoner’s Dilemma. University of Michigan Press, 1965

[26] Goranko V, Jamroga W, Turrini P. Strategic games and truly playable effectivity functions. Autonomous Agents and Multi-Agent Systems, 2013, 26(2): 288-314

[27] Pauly M. Logic for Social Software. Dissertation for the Doctoral Degree. University of Amsterdam, 2001

[28] Marker D. Model Theory: An Introduction (Graduate Texts in Mathematics, Vol. 217). Springer Press, 2002

[29] Ditmarsch van H, Hoek van der W, Kooi B. Dynamic Epistemic Logic. Springer Press, 2007

[30] Vardi M Y. Branching vs. linear time: Final showdown. In: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2001, 1-22

[31] Emerson E A. Temporal and modal logic. Handbook of Theoretical Computer Science (Volume B): Formal Models and Semantics. NorthHolland Pub. Co./MIT Press, 1990

[32] Ågotnes T, Hoek van der W, Rodr guez-Aguilar J A, Sierra C, Wooldridge M. Multi-modal CTL: completeness, complexity, and an application. Studia Logica, 2009, 92(1): 1-26

[33] Belardinelli F, Lomuscio A. First-order linear-time epistemic logic with group knowledge: an axiomatisation of the monodic fragment. Fundamenta Informaticae, 2011, 106(2-4): 175-190

[34] Belardinelli F, Lomuscio A. Interactions between knowledge and time in a first-order logic for multi-agent systems: completeness results. Journal of Artificial Intelligence Research, 2012, 45: 1-45

[35] Lorini E, Schwarzentruber F. A logic for reasoning about counterfactual emotions. Artificial Intelligence, 2011, 175(3-4): 814-847

[36] Su K, Sattar A, Governatori G, Chen Q. A computationally grounded logic of knowledge, belief and certainty. In: Proceedings of the 4th International Joint Conference on Autonomous Agents and Multiagent Systems. 2005, 149-156

[37] Wu L, Su K, Sattar A, Chen Q, Su J, Wu W. A complete first-order temporal BDI logic for forest multi-agent systems. Knowledge-Based System, 2012, 27: 343-351

[38] Ågotnes T, Hoek van der W, Tennenholtz M, Wooldridge M. Power in normative systems. In: Proceedings of the 8th International Joint Conference on Autonomous Agents and Multiagent Systems. 2009, 145-152

[39] Jamroga W, Ågotnes T. Constructive knowledge: what agents can achieve under imperfect information. Journal of Applied Non-Classical Logics, 2007, 17(4): 423-475

[40] Bulling N, Jamroga W. Comparing variants of strategic ability: how uncertainty and memory influence general properties of games. Autonomous Agents and Multi-Agent Systems, 2014, 28(3): 474-518

[41] Grädel E. Model-checking games for logics of imperfect information. Theoretical Computer Science, 2013, 493: 2-14

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg