Quantified Coalition Logic

1 Introduction

Game theoretic models of cooperation has proved to be a valuable source of techniques and insights for the field of multi-agent systems, and cooperation logics such as Alternating-time Temporal Logic (ATL) [Alur et al., 2002] and Coalition Logic (CL) [Pauly, 2001] have proved to be powerful and intuitive knowledge representation formalisms for such games. Many important properties of cooperative scenarios require quantification over coalitions. However, existing cooperation logics provide no direct facility for such quantification, and expressing such properties therefore requires formulae that are exponentially long in the number of agents. Examples include expressing the notion of a weak veto player [Wooldridge and Dunne, 2004] in CL, or solution concepts from cooperative game theory such as nonemptyness of the core in Coalitional Game Logic [ ˚Agotnes et al., 2006]. An obvious solution would be to extend, for example, ATL, with a first-order-style apparatus for quantifying over coalitions. In such a quantified ATL, one might express the fact that agent i is a necessary component of every coalition able to achieve ϕ by the following formula:

However, adding quantification in such a naive way leads to undecidability over infinite domains (using basic quantificational set theory we can define arithmetic), and very high computational complexity even over finite domains. The question therefore arises whether we can add quantification to cooperation logics in such a way that we can express useful properties of cooperation in games without making the resulting logic too computationally complex to be of practical interest. Here, we answer this question in the affirmative.

We introduce Quantified Coalition Logic (QCL), by modifying the existing cooperation modalities of CL in order to enable quantification. In CL, the basic cooperation constructs are 〈C〉ϕ, meaning that coalition C can achieve ϕ1 ; these operators are in fact modal operators with a neighbourhood semantics. In QCL, we replace these operators with expressions 〈P〉ϕ and [P]ϕ; here, P is a predicate over coalitions, and the two sentences express the fact that there exists a coalition C satisfying property P such that C can achieve ϕ and all coalitions satisfying property P can achieve ϕ, respectively. Thus we add a limited form of quantification to CL without the apparatus of quantificational set theory. We show that the resulting logic, QCL, is exponentially more succinct than CL, while being computationally no worse with respect to the key problem of model checking.

The remainder of the paper is structured as follows. After a brief review of CL, we introduce a language for expressing coalition predicates, and show that the satisfiability problem for this language is NP-complete. We then introduce QCL, and give its complete axiomatization. We show that while QCL is no more expressive than Coalition Logic, it is nevertheless exponentially more succinct, in a precise formal sense. We then extend the language of coalition predicates to talk about the cardinality of coalitions, and show that the corresponding completeness and succinctness results also hold for QCL over this extended language. We illustrate QCL by showing how it can be used to succinctly specify a social choice mechanism, which in CL requires specifications that are exponentially long in the number of agents; we then round off with some conclusions.

1 We adopt a notation which is in line with that in ATL: we use 〈C〉 for 'there is a coalition C such that . . . ' where [Pauly, 2001] uses [C], and we write [C] for Pauly's 〈C〉.

2 Coalition Logic

Since QCL is based on Pauly's Coalition Logic CL [Pauly, 2001], we first briefly introduce the latter. CL is a propositional modal logic, containing an indexed collection of unary modal operators 〈C〉 and [C], where C is a coalition, i.e., a subset of a given set of agents Ag. The intended interpretation of 〈C〉ϕ is that C can achieve ϕ, or, that C is effective for ϕ. Formulae of CL are defined by the following grammar (with respect to a set Φ0 of Boolean variables, and a fixed set Ag of agents):

where p ∈ Φ0 is an atomic proposition and C a subset of Ag. As usual, we use parentheses to disambiguate formulae where necessary, and define the remaining connectives of classical logic as abbreviations: ⊥ ≡ ¬⊤, ϕ → ψ ≡ (¬ϕ) ∨ ψ and ϕ↔ψ ≡ (ϕ→ψ) ∧ (ψ →ϕ).

A model M for (over Φ0, Ag) is a triple M = 〈S, E, π〉 where

• S = {s1, . . . , so} is a finite non-empty set of states;
• E : 2Ag × S → 22S is an effectivity function, where T ∈ E(C, s) is intended to mean that from state s, the coalition C can cooperate to ensure that the next state will be a member of T; and
• π : S → 2Φ0 is a valuation function.

Call the set of all models general models, denoted by Gen. It is possible to define a number of constraints on effectivity functions, depending upon exactly which kinds of scenario they are intended to model [Pauly, 2001, pp.24-39]. Unless stated otherwise, we will assume that our models M are weak playability models M ∈ WP , where effectivity functions are outcome monotonic, i.e., ∀C ⊆ Ag, ∀s ∈ S, ∀X,Y ⊆ S, if X ∈ E(C, s) and X ⊆ Y , then Y ∈ E(C, s), and moreover that effectivity functions satisfy Pauly's weak playability conditions [Pauly, 2001, p.30]. An interpretation for CL is a pair M, s whereM is a model and s is a state inM. The satisfaction relation "|=CL" for CL holds between interpretations and formulae of CL. We say that coalition C can enforce ϕ in s if for some T ∈ E(C, s), ϕ is true in all t ∈ T. That is, C can make a choice such that, irrespective of the others' choices, ϕ will hold. Formally, the satisfaction relation is defined by the following inductive rule (we assume the cases for p, ⊤, negation and disjunction are clear):

The notions of truth of ϕ in a model (M |=CL ϕ) and validity in a class of models C (C |=CL ϕ) are defined as usual. The inference relation ⊢CL for CL is given in table 1 (taken from [Pauly, 2001], but adapted to our notation): it is sound and complete with respect to the class of weak playability models WP ([Pauly, 2001, p. 55]).

3 Quantified Coalition Logic

If we have n agents in Ag, and one wants to express that some coalition can enforce some atomic property p, one needs to enumerate 2n disjunctions of the form 〈C〉p. The idea behind Quantified Coalition Logic (QCL) is to avoid this blowup in the length of formulas. Informally, QCL is a propositional modal logic, containing an indexed collection of unary modal operators 〈P〉ϕ and [P]ϕ. The intended interpretation of 〈P〉ϕ is that there exists a set of agents C, satisfying predicate P, such that C can achieve ϕ. We refer to expressions P as coalition predicates, and we now define a language for coalition predicates; QCL will then be parameterised with respect to such a language. Of course, many coalition predicate languages are possible, with different properties, and later we will investigate another such language. Throughout the remainder of this paper, we will assume a fixed, finite set Ag of agents.

Coalition Predicates: Syntactically, we introduce two atomic predicates subseteq and supseteq, and derive a stock of other predicate forms from these. Formally, the syntax of coalition predicates is given by the following grammar:

where C ⊆ Ag is a set of agents. One can think of the atomic predicates subseteq(C) and supseteq(C) as a stock of 2|Ag|+1 propositions, one for each coalition, which are then to be evaluated in a given coalition Co. The circumstances under which a concrete coalition Co satisfies a coalition predicate P, are specified by a satisfaction relation "|=cp", defined by the following four rules:

Now we can be precise about what it means that "a coalition Co satisfies P": it just means Co |=cp P. We will assume the conventional definitions of implication (→), biconditional (↔), and conjunction (∧) in terms of ¬ and ∨.

Coalitional predicates subseteq(·) and supseteq(·) are in fact not independent. They are mutually definable - due to the fact that the set of all agents Ag is assumed to be finite. We then have that ([ ˚Agotnes and Walicki, 2006]) subseteq(C) ≡ ∧i∈Ag\C ¬supseteq({i}) and supseteq(C) ≡ ∧C ′⊆Ag ,C ̸⊆C ′ ¬subseteq(C ′ ). The reason that we include both types of predicates as primitives is a main motivating factor of this paper: we are interested in succinctly expressing quantification in coalition logic.

We find it convenient to make use of the following derived predicates:

eq(C) ≡ subseteq(C) ∧ supseteq(C) subset(C) ≡ subseteq(C) ∧¬eq(C) supset(C) ≡ supseteq(C) ∧¬eq(C) incl(i) ≡ supseteq({i}) excl(i) ≡ ¬incl(i) any ≡ supseteq(∅) nei(C) ≡ ∨i∈C incl (i ) ei(C) ≡ ¬nei(C)

The reader may note an obvious omission here: we have not introduced any explicit way of talking about the cardinality of coalitions; such predicates will be discussed in Section 4.

We say that a coalition predicate P is Ag-consistent if for some Co ⊆ Ag, we have Co |=cp P, and P is Ag-valid if Co |=cp P for all Co ⊆ Ag.

The model checking problem for coalition predicates is the problem of checking whether, for given Co and P, we have Co |=cp P [Clarke et al., 2000]. It is easy to see that this problem is decidable in polynomial time. The satisfiability problem for coalition predicates is the problem of deciding whether P is consistent. We get the following.

Theorem 1 The satisfiability problem for coalition predicates is NP-complete.

Quantified Coalition Logic: We now present QCL. Its formulae are defined by the following grammar:

Models for CL and QCL are the same. The satisfaction relation for the new operators is as follows.

Readers familiar with modal logic may wonder why we did not introduce the universal coalition modality [P]ϕ as the dual ¬〈P〉¬ϕ. In fact such a definition would not serve the desired purpose. Consider the pattern of quantifiers in the semantics of 〈·〉: ∃∃∀. Taking the dual ¬〈·〉¬ would yield the quantifiers ∀∃∃, rather than the desired ∀∃∀ pattern. Of course, this does not mean that [P]ϕ is not definable from 〈P〉ϕ (and the propositional connectives) in some other way. In fact:

Thus, for expressiveness, 〈C〉 together with the propositionals are adequate connectives, and [P]ϕ is definable. The reason we introduce the box cooperation modality as a separate construct is one of the main motivations in this paper, as discussed before for the different predicate operators: succinctness of expression.

Example QCL Expressions: To get a flavour of the kind of properties we can express in QCL, we present some example QCL formulae. First, note that the conventional CL/ATL ability expression is defined simply as: 〈C〉ϕ ≡ 〈eq(C)〉ϕ. We can also succinctly express properties such as the solution concepts from Qualitative Coalitional Games [Wooldridge and Dunne, 2004]. For example, a weak veto player for ϕ is an agent that must be present in any coalition that has the ability to bring about ϕ: WVETO(C, ϕ) ≡ ¬〈excl(i)〉ϕ. Of course, if no coalition has the ability to achieve ϕ, then this means that every agent is a veto player for ϕ. A strong veto player for ϕ is thus an agent that is both a weak veto player for ϕ and that is a member of some coalition that can achieve ϕ: VETO(i, ϕ) ≡ WVETO(i, ϕ) ∧ 〈incl(i)〉ϕ. A coalition C is weakly minimal for ϕ if no subset of C can achieve ϕ: WMIN(C, ϕ) ≡ ¬〈subset(C)〉ϕ. And C are simply minimal if they are weakly minimal and also able to bring about ϕ: MIN(C, ϕ) ≡ 〈C〉ϕ ∧WMIN(C, ϕ). Finally, GC(C) says that C is the grand coalition: GC(C) ≡ [supset (C )]⊥.

Model Checking: Model checking is currently regarded as perhaps the most important computational problem associated with any temporal/modal logic, as model checking approaches for such logics have had a substantial degree of success in industry [Clarke et al., 2000]. The explicit state model checking problem for QCL is as follows:

Given a modelM, state s inM, and formula ϕ of QCL, is it the case thatM, s |=QCL ϕ?

Notice that in this version of the problem, we assume that the components of the model M are explicitly enumerated in the input. It is known that the corresponding problem for Coalition Logic may be solved in polynomial time O(|M| · |ϕ|) [Pauly, 2001, p.50] (as may the explicit state ATL model checking problem [Alur et al., 2002]). Perhaps surprisingly, the QCL model checking problem is no worse:

Theorem 2 The explicit state model checking problem for QCL may be solved in polynomial time.

Of course, this result is not terribly useful, since it assumes a representation of M that is not feasible, since it is exponentially large in the number of agents and Boolean variables in the system. Implemented model checkers use succinct languages for defining models; for example, the REACTIVE MODULES LANGUAGE (RML) of Alur et al [Alur and Henzinger, 1999]. Assuming an RML representation, Coalition Logic model checking is PSPACE-complete [Hoek et al., 2006], and thus no easier than theorem proving in the same logic [Pauly, 2001, p.60]. It is therefore more meaningful to ask what the model checking complexity of QCL is for such a representation. We only give a very brief summary of RML - space restrictions prevent a complete description; see [Alur and Henzinger, 1999; Hoek et al., 2006] for details.

In REACTIVE MODULES, a system is specified as a collection of modules, which correspond to agents. Here is a (somewhat simplified) example of an RML module:

This agent toggle, controls a single Boolean variable, x . The choices available to the agent at any given time are defined by the init and update rules. The init rules define the choices available to the agent with respect to the initialisation of its variables, while the update rules define the agent's choices subsequently. The init rules define two choices for the initialisation of this variable: assign it the value ⊤ or the value ⊥. Both of these rules can fire initially, as their conditions (⊤) are always satisfied; in fact, only one of the available rules will ever actually fire, corresponding to the "choice made" by the agent on that decision round. With respect to update rules, the first rule says that if x has the value ⊤, then the corresponding choice is to assign it the value ⊥, while the second rule 'does the opposite'. In other words, the agent non-deterministically chooses a value for x initially, and then on subsequent rounds toggles this value.

The following can be proved by an adaption and extension of the proof in [Hoek et al., 2006].

Theorem 3 The model checking problem for QCL assuming an RML representation for models is PSPACE-complete.

This result, we believe, is potentially much more interesting than that for explicit state model checking, since it tells us that QCL model checking is no more complex than Coalition Logic even for a realistic representation of models.

Expressive Power: We now argue that QCL is equivalent in expressive power to Coalition Logic. To begin, consider the following translation τ from QCL formulae to CL formulae. For atoms p and ⊤, τ is the identity, and it distributes over disjunction, and moreover:

We already know from above that we have a translation in the other direction: let us call it δ, with defining clause δ(〈C〉ϕ) = 〈eq(C)〉δ(ϕ).

As an example, suppose Ag = {a, b, c} and let P = (supset ({a})∨supset ({b})∨supset ({c}))∧¬eq({a, b, c}). Now, consider the QCL formula ψ = 〈P〉q. Then τ(ψ) = 〈{a, b}〉q ∨ 〈{a, c}〉q ∨ 〈{b, c}〉q while δ(τ(ψ)) = 〈eq({a, b})〉q ∨ 〈eq({a, c})〉q ∨ 〈eq({b, c})〉q. Hence, one can think of δ(τ(ϕ)) as a normal form for ϕ, where the only coalition predicate in ϕ is eq. That QCL and CL have equal expressive power follows from the fact that the two translations preserve truth.

Theorem 4 Let M be a model, and s a state, and let ϕ be a QCL formula, and ψ a CL formula. Then:

1. M, s |=QCL ϕ iff M, s |=CL τ (ϕ)
2. M, s |=CL ψ iff M, s |=QCL δ(ψ)

Axiomatization: The translations introduced above provide the key to a complete axiomatization of QCL. First, recall Pauly's axiomatization of Coalition Logic (Table 1). Given this, and the translations defined previously, we obtain an axiom system for QCL-formulae as follows. First, QCL includes the δ translation of all the CL axioms and rules, and axioms that state that the δ-translation is correct: see the lower part of Table 2. On top of that, QCL is parametrised by an inference relation ⊢cp for coalition predicates. The axioms for this in Table 2 are taken from [ ˚Agotnes and Walicki, 2006].

Theorem 5

1. ([ ˚Agotnes and Walicki, 2006]) ⊢cp is sound and complete: for any P, |=cp P ⇔ ⊢cp P
2. For any CL formula ϕ, ⊢CL ϕ ⇒ ⊢QCL δ(ϕ)
3. Let ϕ be any QCL formula. Then ⊢QCL ϕ ↔ δ(τ(ϕ)) and, in particular, ⊢QCL ϕ iff ⊢QCL δ(τ (ϕ)).

Theorem 6 (Completeness and Soundness) Let ϕ be an arbitrary QCL-formula. Then: ⊢QCL ϕ iff |=QCL ϕ

Examples of derivable properties include:

These illustrate that we not only have primitive modal operators, but also some kind of operations over them, like negation and conjunction. This of course is very reminiscent of Boolean modal logic, where one studies algebraic operations like complement, meet and join on modal operators [Gargov and Passy, 1987]. We will not pursue the details of the connection here.

Succinctness: Theorem4 tells us that the gain of QCL over CL is not its expressivity. Rather, the advantage of QCL is in its succinctness of representation. For example, for the QCL formula 〈any〉q, the translated CL formula τ(〈any〉q) is exponentially longer, since it has to explicitly enumerate all coalitions in Ag. Is it however generally the case that τ(ϕ) is shorter than ϕ? Since the translation does some computations under |=cp, this is in general not the case. For instance, if P = supseteq({a}) ∧ supseteq({c}) ∧ supseteq({b}) ∧ (subseteq({a, b, c}) ∨ subseteq({a, b, d})), then ψ = 〈P〉q would have as a τ-translation 〈{a, b, c}〉q, which is shorter than the original QCL-formula ψ. But then again, δ(τ(ψ)) is a QCL formula that is equivalent to ψ, but that has a size similar to τ(ψ).

To make this all precise, let us define the length ℓ(ϕ) of both QCL and CL formulas ϕ, as follows:

with

Let ϕ and ψ be X and Y formulas, respectively, where X and Y both range over CL and QCL. Then we say that they are equivalent with respect to some class of models if they have the same satisfying pairs M, s, that is, for each M, s in the class of models it is the case that M, s |=X ϕ iff M, s |=Y ψ. This definition naturally extends to sets of formulas.

In the following theorem we show that QCL is exponentially more succinct than CL, over general models. This notion of relative succinctness is taken from [Lutz, 2006], who demonstrates that public announcement logis is more succinct than epistemic logic.

Theorem 7

There is an infinite sequence of distinct QCL formulas ϕ0, ϕ1, . . . such that, not only is the CL formula τ(ϕi ) equivalent to ϕi for every i ≥ 0, but every CL formula ψi that is equivalent, with respect to general models, to ϕi has the property ℓ(ψi ) ≥ 2|ϕi | .

4 Coalition Size

As we noted earlier, an obvious omission from our language of coalition predicates is designated predicates for expressing cardinality properties of coalitions. In this section, we explore extensions to the framework for this purpose. The obvious approach is to introduce primitive coalition predicates geq(n), where n ∈ N, with semantics as follows:

Given this predicate, we can define several obvious derived predicates (see also [ ˚Agotnes and Alechina, 2006] for a discussion of a similar language).

The first natural question is whether geq(n) is definable in QCL. Indeed it is:

However, we again see that such a definition leads to exponentially large formulae, which justifies extending the predicate language of QCL with an atomic coalition predicate geq(n) for every n ∈ N. Call the resulting logic QCL(≥), and let |=cp≥ and |=QCL(≥) denote the satisfiability relations for QCL(≥) predicates and QCL(≥) formulae, respectively. Once again, the gain is not expressiveness but succinctness. As another example of the added succinctness, consider the CL formula 〈C〉p. In QCL this cannot in general be written by any less complex formula than 〈subseteq(C) ∧ supseteq(C)〉p, but in QCL(≥) it can be simplified somewhat to 〈supseteq(C)∧¬geq(|C|+1)〉p (which in general is simpler since one of the enumerations of the agents in C is replaced by a number).

A subtle but important issue when reasoning with the logic is the way in which the natural number argument of the geq(. . .) predicate is represented. Suppose, (following standard practice in complexity theory), that we represent the argument in binary. Now, we ask whether a given coalition predicate P is satisfiable, where P contains a constraint geq(n). Now checking the satisfiability of such constraints is not obviously in NP. The problem is that the witness C to the satisfiability of P is exponentially larger than the constraint geq(n). Of course, if we express the natural number n in unary, then this is not an issue. But unary is not a realistic or practical representation for numbers. It turns out, however, that we do in fact get NP completeness for the satisfiability problem also for QCL(≥), although the argument requires some more work. The reason is that we can use an efficient encoding of the witness C . This was shown by [ ˚Agotnes and Alechina, 2006] for a similar problem (cf. Section 5).

Let Ag(P) and subp(P) denote the set of agents, and the set of sub-predicates, respectively, occurring in a predicate P.

Lemma 1 Any satisfiable QCL(≥) predicate P is satisfied by a coalition consisting of no more than 1 + maxP agents, where 1 +maxP equals

Theorem 8 The satisfiability problem for QCL(≥) coalition predicates is NP-complete.

It is straightforward to lift the translation τ from QCL to CL to the case when also the additional predicates of QCL(≥) are allowed, and it is easy to see that Theorem 4 holds also for QCL(≥) formulae. For axiomatisation, we only need to add axioms for the geq(n) predicates to the predicate calclulus. That can be achieved simply by adding (1) as an axiom

Table 3: Extra predicate calculus axioms for QCL(≥).

schema. A more "direct" axiomatisation of geq(n) is shown in Table 3, taken from [ ˚Agotnes and Alechina, 2006]. Let ⊢cp≥ denote derivability in the QCL predicate calculus (from Table 2) extended with the axioms in Table 3. The following is easily obtained from a similar result in [ ˚Agotnes and Alechina, 2006]:

Lemma 2 The QCL(≥) predicate calculus is sound and complete: for any QCL(≥) predicate P, |=cp≥ P ⇔ ⊢cp≥ P

Let ⊢QCL(≥) denote derivability in the system obtained by replacing ⊢cp with ⊢cp≥ in the definition of ⊢QCL (Table 2).

Theorem 9 (Completeness and Soundness) Let ϕ be a QCL(≥)-formula. Then: ⊢QCL(≥) ϕ iff |=QCL(≥) ϕ

To illustrate the use of QCL(C) for reasoning about multiagent systems, consider the expression of majority voting:

An electorate of n voters wishes to select one of two outcomes ω1 and ω2. They want to use a simple majority voting protocol, so that outcome ωi will be selected iff a majority of the n voters state a preference for it. No coalition of less than majority size should be able to select an outcome, and any majority should be able to choose the outcome (i.e., the selection procedure is not influenced by the "names" of the agents in a coalition). One outcome must be selected, but both outcomes should not be selected simultaneously.

We express these requirements as follows. First: any majority should be able to select an outcome.

No coalition that is not a majority can select an outcome.

Either outcome ω1 or ω2 must result.

Both outcomes cannot be selected simultaneously.

Notice that majority voting cannot be succinctly specified using regular Coalition Logic.

5 RelatedWork and Conclusions

Quantified Coalition Logic adds a limited but useful form of quantification to Coalition Logic, which is computationally tractable. The motivation is succinctness rather than expressiveness: QCL is exponentially more expressive than CL.

While first-order temporal logics have been studied in the literature, and CL can be seen as the next-time fragment of ATL which again is a generalisation of the branchingtime temporal logic Computational Tree Logic (CTL), we are not aware of any other works on quantification in CL or ATL. Lately, there has been some work on generalising the coalition modalities in another direction: to explicitly include actions and strategies [van der Hoek et al., 2005; ˚Agotnes, 2006].

Opportunities for future work include a more detailed understanding of the relationship between QCL and Boolean modal logic.