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. (shrink)

Boolean games are a logical setting for representing strategic games in a succinct way, taking advantage of the expressive power and conciseness of propositional logic. A Boolean game consists of a set of players, each of which controls a set of propositional variables and has a specific goal expressed by a propositional formula. We show here that Boolean games are a very simple setting, yet sophisticated enough, for analysing the formation of coalitions. Due to the fact that players have dichotomous (...) preferences, the following notion emerges naturally: a coalition in a Boolean game is efficient if it has the power to guarantee that all goals of the members of the coalition are satisfied. We study the properties of efficient coalitions. (shrink)

Many problems in Multi-Agent Systems (MASs) research are formulated in terms of the abilities of a coalition of agents. Existing approaches to reasoning about coalitional ability are usually focused on games or transition systems, which are described in terms of states and actions. Such approaches however often neglect a key feature of multi-agent systems, namely that the actions of the agents require resources. In this paper, we describe a logic for reasoning about coalitional ability under resource constraints in the probabilistic (...) setting. We extend Resource-bounded Alternating-time Temporal Logic (RB-ATL) with probabilistic reasoning and provide a standard algorithm for the model-checking problem of the resulting logic Probabilistic resource-bounded ATL (pRB-ATL). We implement model-checking algorithms and present experimental results using simple multi-agent model-checking problems of increasing complexity. (shrink)

We introduce a reciprocity criterion for coalition formation among goal-directed agents, which we call the indecomposable do-ut-des property. It refines an older reciprocity property, called the do-ut-des or give-to-get property by considering the fact that agents prefer to form coalitions whose components cannot be formed independently. A formal description of this property is provided as well as an analysis of algorithms and their complexity. We provide an algorithm to decide whether a coalition has the desired property, and we show that (...) the problem to verify whether a single coalition satisfies the property is tractable. Moreover, we provide an algorithm to search all the sub-coalitions of a given coalition satisfying the new property. Even if this problem is not computationally tractable, we show that in several cases, also the complexity of this problem may decrease considerably. (shrink)

Qualitative Coalitional Games are a variant of coalitional games in which an agent's desires are represented as goals that are either satisfied or unsatisfied, and each choice available to a coalition is a set of goals, which would be jointly satisfied if the coalition made that choice. A coalition in a QCG will typically form in order to bring about a set of goals that will satisfy all members of the coalition. Our goal in this paper is to develop and (...) study logics for reasoning about QCGs. We begin by introducing a logic for reasoning about “static” QCGs, where participants play a single game, and we then introduce and study Temporal QCGs , i.e., games in which a sequence of QCGs is played. In order to represent and reason about such games, we introduce a linear time temporal logic of QCGs, called ℒ. We give a complete axiomatisation of ℒ, use it to investigate the properties of TQCGs, identify its expressive power, establish its complexity, characterise classes of TQGCs with formulas from our logical language, and use it to formulate several solution concepts for TQCGs. (shrink)