Quantified Coalition Logic

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 properties as "there exists a coalition C satisfying property P such that C can achieve Phi". 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.