A first-order coalition logic for BDI-agents

doi:10.1007/s11704-015-4591-2

Front. Comput. Sci.

2016, Vol. 10

Issue (2) : 233-245 https://doi.org/10.1007/s11704-015-4591-2

RESEARCH ARTICLE

A first-order coalition logic for BDI-agents

Qingliang CHEN¹,Kaile SU^1,²,Abdul SATTAR²,Xiangyu LUO^3,^*(

),Aixiang CHEN⁴

1. Department of Computer Science, Jinan University, Guangzhou 510632, China
2. Institute for Integrated and Intelligent Systems, Griffith University, Brisbane 4111, Australia
3. College of Computer Science and Technology, Huaqiao University, Xiamen 361021, China
4. School of Mathematics and Statistics, Guangdong University of Finance and Economics, Guangzhou 510320, China

Download: PDF(404 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): Xiangyu LUO

Just Accepted Date: 23 July 2015 Issue Date: 16 March 2016

Cite this article:

Qingliang CHEN,Kaile SU,Abdul SATTAR, et al. A first-order coalition logic for BDI-agents[J]. Front. Comput. Sci., 2016, 10(2): 233-245.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-015-4591-2
https://academic.hep.com.cn/fcs/EN/Y2016/V10/I2/233

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 https://doi.org/10.1016/S1574-6526(07)03024-6
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 https://doi.org/10.1093/logcom/12.1.149
7	Alur R, Henzinger T A, Kupferman O. Alternating-time temporallogic. Journal of the ACM, 2002, 49(5): 672–713 https://doi.org/10.1145/585265.585270
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 https://doi.org/10.1023/A:1026185103185
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 https://doi.org/10.1007/s11229-008-9363-1
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 https://doi.org/10.1016/j.artint.2008.08.004
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 https://doi.org/10.1145/1324249.1324285
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 https://doi.org/10.1016/j.tcs.2005.07.043
20	Pnueli A. The temporal logic of programs. In: Proceedings of the 18thAnnual Symposium on Foundations of Computer Science. 1977, 46–57 https://doi.org/10.1109/sfcs.1977.32
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 https://doi.org/10.1007/s10458-012-9192-y
25	Jamroga W, Penczek W. Specification and verification of multi-agentsystems. Lecture Notes in Computer Science, 2012, 7388: 210–263 https://doi.org/10.1007/978-3-642-31485-8_6
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 https://doi.org/10.1109/ICMAS.2000.858426
28	Fitting M. Barcan both ways. Journal of Applied Non-Classical Logics,1999, 9(2–3): 329–344 https://doi.org/10.1080/11663081.1999.10510970
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 https://doi.org/10.1007/978-3-540-74915-8_4
32	Sistla A P, Clarke E M. The complexity of propositional linear temporallogics. Journal of the ACM, 1985, 32(3): 733–749 https://doi.org/10.1145/3828.3837
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 https://doi.org/10.1007/3-540-45657-0_29
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 https://doi.org/10.1007/978-3-642-02658-4_55
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 https://doi.org/10.1007/978-3-540-27813-9_41
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 https://doi.org/10.1007/bfb0028774
39	Blackburn P, de Rijke M, Venema Y. Modal Logic. Cambridge: Cambridge University Press, 2001 https://doi.org/10.1017/CBO9781107050884
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 https://doi.org/10.1007/s11704-014-4097-3
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 https://doi.org/10.1145/1324249.1324264
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 https://doi.org/10.3166/jancl.19.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 https://doi.org/10.4204/eptcs.146.4
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 https://doi.org/10.1016/j.artint.2015.01.005
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 https://doi.org/10.1016/j.tcs.2012.10.033
51	Ågotnes T, Alechina N. A logic for reasoning about knowledge of unawareness. Journal of Logic, Language and Information, 2014, 23(2):197–217 https://doi.org/10.1007/s10849-014-9201-4
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 https://doi.org/10.1007/s10458-013-9231-3

[1]

FCS-0233-14591-XYL_suppl_1

Download

[1]	Qingliang CHEN,Kaile SU,Yong HU,Guiwu HU. A complete coalition logic of temporal knowledge for multi-agent systems[J]. Front. Comput. Sci., 2015, 9(1): 75-86.
[2]	Silvano COLOMBO TOSATTO,Pierre KELSEN,Qin MA,Marwane el KHARBILI,Guido GOVERNATORI,Leendert van der TORRE. Algorithms for tractable compliance problems[J]. Front. Comput. Sci., 2015, 9(1): 55-74.

Viewed

Full text

Abstract

Cited

Shared

Discussed