Quantified coalition logic

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 properties as "there exists a coalition C satisfying property P such that C can achieve ". We give an axiomatization of QCL, and show that while it is no more expressive than Coalition Logic, it is exponentially more succinct. The time complexity of QCL model checking for symbolic and explicit state representations is shown to be no worse than that of 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.

• Type: Journal
• Year: 2008
• Where: SYNTHESE
• Authors: Thomas Ågotnes, Wiebe van der Hoek, Michael Wooldridge
• Keywords: Coalition Logic, Game-like Multi-agent Systems, Popular Formalism, SYNTHESE 2008