Abstract
We add a limited but useful form of quantification to Coalition Logic, a popular formalism for reasoning about cooperation in game-like multi-agent systems. The basic constructs of Quantified Coalition Logic (QCL) allow us to express such properties as “every coalition satisfying property P can achieve φ” and “there exists a coalition C satisfying property P such that C can achieve φ”. We give an axiomatisation of QCL, and show that while it is no more expressive than Coalition Logic, it is nevertheless exponentially more succinct. The complexity of QCL model checking for symbolic and explicit state representations is shown to be no worse than that of Coalition Logic, and satisfiability for QCL is shown to be no worse than satisfiability for Coalition Logic. We illustrate the formalism by showing how to succinctly specify such social choice mechanisms as majority voting, which in Coalition Logic require specifications that are exponentially long in the number of agents.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Ågotnes T. (2006) Action and knowledge in alternating-time temporal logic. Synthese 149(2): 377–409
Ågotnes, T., van der Hoek, W., & Wooldridge, M. (2006). On the logic of coalitional games. In Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS-2006), Hakodate, Japan.
Ågotnes, T., & Walicki, M. (2006). Complete axiomatizations of finite syntactic epistemic states. In M. Baldoni, U. Endriss, A. Omicini, & P. Torroni (Eds.), Declarative Agent Languages and Technologies III: Third International Workshop, DALT 2005, Utrecht, The Netherlands, July 25, 2005. Selected and revised papers of lecture notes in computer science (LNCS) (Vol. 3904, pp. 33–50). Heidelberg: Springer.
Alur R., Henzinger T.A. (1999) Reactive modules. Formal Methods in System Design 15(11): 7–48
Alur R., Henzinger T.A., Kupferman O. (2002) Alternating-time temporal logic. Journal of the ACM 49(5): 672–713
Clarke E.M., Grumberg O., Peled D.A. (2000) Model checking. The MIT Press, Cambridge, MA
Dunne P.E., van der Hoek W., Wooldridge M. (2007) A logical characterisation of qualitative coalitional games. Journal of Applied Non-Classical Logics 17(4): 477–509
Gallier, J. (1987). Logic for computer science: Foundations of automatic theorem proving. Wiley.
Gargov, G., & Passy, S. (1987). A note on Boolean modal logic. In Mathematical logic and applications (pp. 253–263). Plenum Press.
Lutz, C. (2006). Complexity and succinctness of public announcement logic. In Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS-2006), Hakodate, Japan.
Papadimitriou C.H. (1994) Computational complexity. Addison-Wesley, Reading, MA
Pauly, M. (2001). Logic for social software. Ph.D. thesis, University of Amsterdam. ILLC Dissertation Series 2001-10.
van der Hoek, W., Jamroga, W., & Wooldridge, M. (2005a). A logic for strategic reasoning. In Proceedings of the Fourth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS-2005) (pp. 157–153). The Netherlands: Utrecht.
van der Hoek, W., & Lomuscio, A., & Wooldridge, M. (2005b). On the complexity of practical ATL model checking. In Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS-2006), Hakodate, Japan.
Wooldridge M., Dunne P.E. (2004) On the computational complexity of qualitative coalitional games. Artificial Intelligence 158(1): 27–73
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Ågotnes, T., van der Hoek, W. & Wooldridge, M. Quantified coalition logic. Synthese 165, 269–294 (2008). https://doi.org/10.1007/s11229-008-9363-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11229-008-9363-1