A first-order coalition logic for BDI-agents

Abstract

Coalition logic (CL) enables us to model the strategic abilities and specify what a group of agents can achieve whatever the other agents do. However, some rational mental attitudes of the agents are beyond the scope of CL such as the prestigious beliefs, desires and intentions (BDI) which is an interesting and useful epistemic notion and has spawned substantial amount of studies in multi-agent systems. In this paper, we introduce a first-order coalition BDI (FCBDI) logic for multi-agent systems, which provides a semantic glue that allows the formal embedding and interaction of BDI, coalition and temporal operators in a first-order language. We further introduce a semantic model based on the interpreted system model and present an axiomatic system that is proved sound and complete with respect to the semantics. Finally, it is shown that the computational complexity of its model checking in finite structures is PSPACE-complete.

Keywords

coalition logic / BDI logic / complete axiomatization / computational complexity

References

[1] Van der Hoek W, Wooldridge M. Logics for multi-agent systems. In: Weiss G, ed. Multi-Agent Systems (2nd ed.). Cambridge: MIT Press, 2013, 671–810

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

[3] Van der Hoek W, Wooldridge M. Multi-agent systems. Foundations of Artificial Intelligence, 2008, 3: 887–928

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

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

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

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

[8] Belnap N, Perloff M, Xu M. Facing the Future: Agents and Choices in Our Indeterminist World. Oxford: Oxford University Press, 2001

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

[10] Å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

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

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

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

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

[15] Walther D, Van der Hoek W, Wooldridge M. Alternating-time temporallogic with explicit strategies. In: Proceedings of the 11th Conferenceon Theoretical Aspects of Rationality and Knowledge. 2007, 269–278

[16] 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

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

[18] Rao A S,Georgeff M P. BDI agents: from theory to practice. In: Proceedings of the 1st International Conference on Multiagent Systems. 1995, 312–319

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

[20] Pnueli A. The temporal logic of programs. In: Proceedings of the 18thAnnual Symposium on Foundations of Computer Science. 1977, 46–57

[21] Su K, Sattar A, Wang K, Luo X, Governatori G, Padmanabhan V. Observation-based model for BDI-agents. In: Proceedings of the 20thNational Conference on Artificial Intelligence. 2005, 190–195

[22] Goranko V, Jamroga W, Turrini P. Strategic games and truly playable effectivity functions. In: Proceedings of the 10th International Conferenceon Autonomous Agents and Multiagent Systems. 2011, 727–734

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

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

[25] Jamroga W, Penczek W. Specification and verification of multi-agentsystems. Lecture Notes in Computer Science, 2012, 7388: 210–263

[26] Bratman ME. Intention, Plans, and Practical Reason. Cambridge: Harvard University Press, 1987

[27] Wooldridge M. Computationally grounded theories of agency. In: Proceedings of the 4th International Conference on Multi-Agent Systems. 2000, 13–22

[28] Fitting M. Barcan both ways. Journal of Applied Non-Classical Logics,1999, 9(2–3): 329–344

[29] Enderton H B. A Mathematical Introduction to Logic. 2nd ed. NewYork: Academic Press, 2000

[30] Cresswell M, Hughes G. A New Introduction to Modal Logic. London: Routledge, 1996

[31] Dawar A. Model-checking first-order logic: automata and locality. Lecture Notes in Computer Science, 2007, 4646: 6

[32] Sistla A P, Clarke E M. The complexity of propositional linear temporallogics. Journal of the ACM, 1985, 32(3): 733–749

[33] Wooldridge M, Ågotnes T, Dunne P E, Van der Hoek W. Logic for automated mechanism design—a progress report. In: Proceedings of the 22nd AAAI Conference on Artificial Intelligence. 2007, 9–17

[34] Kacprzak M, Nabialek W, Niewiadomski A, Penczek W, Pólrola A,Szreter M, Wozna B, Zbrzezny A. VerICS 2007 — a model checker for knowledge and real-time. Fundamenta Informaticae, 2008, 85(1–4): 313–328

[35] Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2: an opensource tool for symbolicmodel checking. In: Proceedings of the 14th International Conferenceon Computer Aided Verification. 2002, 359–364

[36] Lomuscio A, Qu H, Raimondi F. MCMAS: a model checker for the verification of multi-agent systems. In: Proceedings of the 21st International Conference on Computer Aided Verification. 2009, 682–688

[37] Gammie P, Van der Meyden R. MCK: model checking the logic of knowledge. In: Proceedings of the 16th International Conference on Computer Aided Verification. 2004, 479–483

[38] Alur R, Henzinger T A, Mang F Y C, Qadeer S, Rajamani S K, TasiranS. MOCHA: modularity in model checking. In: Proceedings of the10th International Conference on Computer Aided Verification. 1998,521–525

[39] Blackburn P, de Rijke M, Venema Y. Modal Logic. Cambridge: Cambridge University Press, 2001

[40] Chen Q, Su K, Hu Y, Hu G. A complete coalition logic of temporal knowledge for multi-agent systems. Frontiers of Computer Science, 2015, 9(1): 75–86

[41] Broersen J, Herzig A, Troquard N. A normal simulation of coalitionlogic and an epistemic extension. In: Proceedings of the 11th Conferenceon Theoretical Aspects of Rationality and Knowledge. 2007, 92–101

[42] 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

[43] Huang X, Luo C. A logic of probabilistic knowledge and strategy. In: Proceedings of International Conference on Autonomous Agents and Multi-Agent Systems. 2013, 845–852

[44] Huang X, Van der Meyden R. A temporal logic of strategic knowledge. In: Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning. 2014

[45] Belardinelli F. Reasoning about knowledge and strategies: epistemic strategy logic. In: Proceedings of the 2nd International Workshop on Strategic Reasoning. 2014, 27–33

[46] Cermák P, Lomuscio A, Mogavero F, Murano A. MCMAS-SLK: amodel checker for the verification of strategy logic specifications. In: Proceedings of the 26th International Conference on Computer Aided Verification. 2014, 525–532

[47] Huang X. Bounded model checking of strategy ability with perfect recall. Artificial Intelligence, 2015, 222: 182–200

[48] Huang X, Van der Meyden R. Symbolic model checking epistemic strategy logic. In: Proceedings of the 28th AAAI Conference on Artificial Intelligence. 2014, 1426–1432

[49] Jamroga W, Murano A. Module checking of strategic ability. In: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems. 2015, 227–235

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

[51] Ågotnes T, Alechina N. A logic for reasoning about knowledge of unawareness. Journal of Logic, Language and Information, 2014, 23(2):197–217

[52] Gutierrez J, Harrenstein P, Wooldridge M. Reasoning about equilibriain game-like concurrent systems. In: Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning. 2014

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

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg