# rich_coalitional_resource_games__f17fe4d0.pdf

Rich Coalitional Resource Games

Nicolas Troquard The KRDB Research Centre Faculty of Computer Science Free University of Bozen-Bolzano Piazza Domenicani, 3 I-39100 Bozen-Bolzano BZ, Italy

We propose a simple model of interaction for resourceconscious agents. The resources involved are expressed in fragments of Linear Logic. We investigate a few problems relevant to cooperative games, such as deciding whether a group of agents can form a coalition and act together in a way that satisfies all of them. In terms of solution concepts, we study the computational aspects of the core of a game. The main contributions are a formal link with the existing literature, and complexity results for several classes of models.

Introduction One crucial theme in multi-agent systems is the one of resource-conscious agents. As the research in multiagent systems is advancing and one can predict its future widespread implementation in real-world systems, one needs to acknowledge that the agents evolving in the real world have limited access to resources. They have to seek after resource objectives and compete for those resources. When unable to attain a resource alone, they might have to form coalitions. In their abstract definition, coalitional games are presented as a tuple (Ag, VAL), where Ag is a set of agents, and VAL : 2Ag R is a coalition collective value. Typically, we assume that VAL( ) = 0. We call simple game a coalitional game such that for every coalition C N, we have VAL(C) = 0 or VAL(C) = 1. Where these utilities come from however is not part of the description. Here, each player i of a game is endowed with a multiset of resources eni. An action for Player i consists in contributing a subset of eni. Then, each player i has a set of goals Gi, which is a set of resources, represented by formulas of some resourcesensitive logic LOG. In the resulting coalition games, the valuation function will depend of these individual endowments and goals. Example 1. Consider the following setting that will be fully formalised later. Player 1 is happy with bacon, Player 2 is happy with either bacon or an egg, and Player 3 is happy with an omelet. Player 1 is endowed with one egg and the capacity of using an egg to make an omelet. Player 2 is endowed with bacon. Player 3 is endowed with one egg.

Copyright c 2018, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

Player 2 is self-reliant as she can eat her bacon and be happy. To make Player 1 happy as well, this bacon must be used towards the happiness of Player 1. In this case, it is Player 1 s egg that will be used towards Player 2 s happiness. To add Player 3 into the happy team, Player 3 can provide his egg, which can be transformed into an omelet using Player 1 s still uncommitted capacity of transforming and egg into an omelet. The value of the coalitions {2}, {1, 2}, and {1, 2, 3} is thus 1. In this paper, we propose simple models of interaction capable of representing and reasoning about scenarios such as Example 1, where resources can be intricately consumed, transformed, and produced by agents. They are compact coalitional games reminiscent of (Wooldridge and Dunne 2006) and (Bachrach and Rosenschein 2008). We propose what is effectively an extension of coalitional resource games (Wooldridge and Dunne 2006) that takes advantage of resource-sensitive logics. The exact resource-sensitive logic will be a parameter LOG, which can be instantiated with any variant and fragment of Linear Logic (Girard 1987), Bunched Logic (O Hearn and Pym 1999), etc.

We briefly present the Linear Logic formalism in the next section. The results of this paper will be applicable to every fragment and variant of Linear Logic mentioned there. In Linear Logic, a formula can be interpreted as a resource. It has been used before in social choice and game theory, e.g., (Porello and Endriss 2010a; 2010b; De Young and Sch urmann 2012; Troquard 2016). The propositional language of Linear Logic can distinguish simultaneous availability of resources (A B), deterministic (A&B) and non-deterministic (A B) choices between resources, resource transformations (A B), and anti-resources ( A). For instance, $1 ($1 $1) 1 captures a capacity of gambling, where if an agent gives $1, they receive $2 or nothing (the vacuous resource 1), and do not get to choose. On the other hand, $10 fish & meat captures a capacity of buying a meal, where if an agent gives $10, they receive a meal of fish or a meal of meat, and they choose which one. Moreover, the resource-consciousness is a built-in feature of the entailment of these logics. For instance, it is not the case that $1 $1 $1, unlike its classical counterpart $1 $1 $1.

Having resources and goals represented in the same way has important consequences. The language of Linear Logic

The Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18)

allows us to represent at the same level of abstraction, simultaneous resources, two kinds of disjunctions, and crucially, resource-transforming capacities (e.g., transforming one egg into an omelet). This becomes all the more significant when the resources are subject to a series of transforming activities. In contrast, in the coalitional resource games from (Wooldridge and Dunne 2006), resources become goals, and game over . Furthermore, using Linear Logic, we can exploit the existing research in logic proofs and automated proofs. Through the Curry-Howard correspondence between proofs and programs (see, e.g., (Gabbay and de Queiroz 1992)), an exciting perspective is the possibility to interpret the logical proofs as rigorous programs to be executed by the coalitions. Hence, one goal of this research is the automated generation of cooperative plans, where the resources can be subjected to a series of transforming activities by the agents.

We first provide a brief summary of the formal aspects of Linear Logic that we use in this paper. We present the coalitional resource games (CRG) from (Wooldridge and Dunne 2006) and we introduce the class of rich coalitional resource games (RCRG). We then propose a translation of CRGs into RCRGs that preserves the set of goals that are feasible for the coalitions. Next, we study a few decision problems: deciding whether a coalition is winning, deciding whether a player is a veto player, deciding whether a player is a dummy player, and deciding whether the core of a game is non-empty. A formalization of Example 1 is then presented before the conclusion.

Linear Logic A good introduction to Linear Logic and its variants is (Troelstra 1992). MLL is the multiplicative fragment of Linear Logic: A ::= 1| |p| A|A A|A A|A A, where p is an atomic formula. MALL is the fragment with both additive and multiplicative operators: A ::= |0|1| |p| A|A A|A A|A A|A & A|A A. We say that the logic is affine when it admits the structural rule of weakening (W). We only present the sequent rules for affine MALL that are used in this paper. See (Troelstra 1992) for the complete sequent calculus. A, and B are formulas. Γ, Γ , Δ, and Δ are sequences of zero or more formulas.

ax A A 1R 1 Γ, A, B, Γ Δ E Γ, B, A, Γ Δ Γ Δ W Γ, A Δ

Γ A, Δ Γ B, Δ

R Γ, Γ A B, Δ, Δ Γ, A, B Δ L Γ, A B Δ Γ A, Δ R Γ B A, Δ

Γ A, Δ Γ , B Δ

L Γ, Γ , A B, Δ Δ Γ A, Δ L Γ, A Δ Γ, A Δ R Γ A, Δ Affine MLL is obtained by removing the rules involving &, , and 0. MALL is the logic obtained by removing the rules (W) (of which only one is used here). MLL is obtained by removing the rules (W) and the rules involving &, , and 0 (of which only one is used here). We quickly summarize the complexity of some fragments and variants of Linear Logic. MALL is PSPACEcomplete; MLL is NP-complete; Affine MLL is NPcomplete; Affine MALL is PSPACE-complete; Intuition-

istic MALL is PSPACE-complete; Intuitionisitc MLL is NP-complete. First-Order MLL is NP-complete and First Order MALL is NEXPTIME-complete. Something particularly interesting is that these fragments of Linear Logic behave well computationally also in the first-order case. It is in contrast with First-Order classical logic which is undecidable. First-Order MLL is NP-complete and First-Order MALL is NEXPTIME-complete. See (Lincoln et al. 1992; Kanovich 1994).

Coalitional Games We first present the coalitional resource games from (Wooldridge and Dunne 2006). Then we introduce a variant that makes use of Linear Logic to represent rich resources.

Coalitional Resource Games Coalitional resource games were introduced in (Wooldridge and Dunne 2006).

Definition 2. A coalitional resource game (CRG) is a tuple Γ = (Ag, G, (Gi)i Ag, R, en, req) where:

Ag = {a1, . . . , an} is a set of agents; G = {g1, . . . , gm} is a set of possible goals; R = {r1, . . . , rt} is a set of resources; for each agent i Ag, the set Gi G collects the goals agent i would be satisfied with; en : Ag R N is an endowment function; req : G R N is a requirement function.

In addition, we assume g G, r R : req(g, r) > 0.

Endowment and requirement functions are naturally extended. We define: en(C, r) = i C en(i, r) and req(H, r) =

g H req(g, r). We say that a set of goals H satisfies agent i if H Gi = ; it satisfies a coalition C if it satisfies all its members. We define the set of sets of goals that satisfy coalition C as satΓ(C) = {H G | i C, H Gi = }. We say that a set of goals H is feasible for a coalition when the coalition is endowed with enough resources to achieve all the goals in H. We define the set of feasible sets of goals of coalition C as feasΓ(C) = {H G | r R, req(H, r) en(C, r)}. Finally, we denote the set of sets of goals that are feasible by coalition C and satisfy coalition C with sf Γ(C) = satΓ(C) feasΓ(C).

Rich Coalitional Resource Games We propose a variant of coalitional resource games that makes use of resource-sensitive logics. The exact resourcesensitive logic is a parameter LOG, which can be instantiated with any variant and fragment of Linear Logic (Girard 1987). We assume that the language of LOG is at least the one of MLL. In RCRGs, resources and goals are the same type of objects: LOG formulas. Resources can then be combined and transformed following the rules of LOG so as to yield goals. As the translation from CRGs to RCRGs will make clear in the next section, the requirement function of CRGs can be built in the very formulas that represent endowed resources.

Definition 3. A rich coalitional resource game (RCRG) is a tuple Γ = (Ag, G, (Gi)i Ag, en) where: Ag = {a1, . . . , an} is a finite set of agents; for each agent i Ag, the finite non-empty set Gi LOG collects the goals agent i would be satisfied with; G is a finite multiset of possible goals. We assume i Ag Gi G; for every i Ag, the finite multiset eni LOG is agent i s endowment. Endowments are naturally extended to coalitions. We define: en C =

i C eni. We say that a multiset of goals H G satisfies coalition C Ag if there is (g1, . . . , gn) i Ag Gi such that

i C{gi} H. We define the set of multisets of goals that satisfy coalition C as satΓ(C) = {H G | H satisfies C}. We say that a multiset of goals H G is feasible for a coalition C when there is E en C such that E H. We define the set of multisets of goals for which the coalition C is feasible as follows: feasΓ(C) = {H G | H is feasible for C}. The set of multisets of goals that are feasible by coalition C and satisfy coalition C is defined as before with sf Γ(C) = satΓ(C) feasΓ(C).

Restricted classes of RCRG. We will successively focus our attention on some variants of RCRG. There will be three varying dimensions. (i) Affine RCRGs add to the deductive power of the underlying logic LOG. (ii) MLL and MALL RCRGs modify the expressivity of the underlying logic LOG. (iii) One-goal RCRGs adds constraints on the number of goals of each player. Weakening, rule (W), is a structural rule that accounts for the monotonicity of the entailment of a logic. Linear Logic does not admit the weakening rule, but affine logic does.1 However, it has generally no effect on the complexity of the problem of sequent validity. Sequent validity in MLL is NPcomplete with or without weakening and sequent validity in MALL is PSPACE-complete with or without weakening. On the other hand, whether LOG admits weakening or not will have dramatic consequences for the algorithmic solutions to the decision problems in RCRG. Definition 4. An affine RCRG is an RCRG instantiated with LOG admitting weakening (rule (W)). The exact syntactic variant chosen for LOG will of course have an effect on the complexity results. Definition 5. A MLL RCRG is an RCRG instantiated with LOG being MLL. A MALL RCRG is an RCRG instantiated with LOG being MALL. Finally, we propose a variant that imposes a restriction on the number of goals for each player. Definition 6. A one-goal RCRG is an RCRG Γ = (Ag, G, (Gi)i Ag, en) where |Gi| = 1. Remark 7. One-goal RCRGs, and MALL RCRGs in particular, are often enough . In CRGs, multi-goals are essentially disjunctive goals: a player is happy when one of

1When a logic is affine we have A B A, while it is not the case in Linear Logic in general. In other words, extra resources can be disposed of.

her goals is satisfied. With the Linear Logic language of resources, we can satisfyingly capture disjunctive goals in one-goal RCRGs. We can even decide which kind of nondeterministic goal to use! We can use the connective , e.g., egg bacon, to indicate that the player wants either egg or bacon. (We will use this goal in the formalisation of Example 1 later.) We can use the connective &, e.g., egg&bacon to emphasize that the player wants to retain the choice between egg and bacon.

From CRGs to MLL RCRGs Let Γ = (Ag, G, R, (Gi)i Ag, en, req) be a CRG. For every goal g G, we reserve an atomic proposition pg in LOG. For every resource r R, we reserve an atomic proposition pr in LOG. For every goal g G, we write

pr . . . pr req(g,r) times

It is a formula of LOG that characterises the requirement in terms of resources of the goal g. We build the RCRG ΓR = (Ag R, GR, (GR i )i Ag R, en R) as follows:

Ag R = Ag; GR = g G{pg, . . . , pg |Ag R| times

GR i = {pg | g Gi}; en R i is a multiset of formulas in LOG containing en(i, r) instances of the atomic proposition pr for every resource r R and one instance of the formula ρg pg for every goal g G:

r R {pr, . . . , pr en(i,r)

g G {ρg pg}

Observe that we do not use any additive operator. It is enough to define the constructed ΓR to be an MLL RCRG. Remark 8. This translation from CRGs to RCRGs is meant as a rigorous and formal comparison of RCRGs with the existing literature. This translation, however, is not meant to suggest that CRGs problems should be solved within the framework of RCRGs. Indeed, the proposed translation from CRGs to RCRGs obviously causes a blowup when the numbers in the CRG are encoded in binary. Interestingly, in (Wooldridge and Dunne 2006), the complexity results for CRGs are strong : the problems stay in the same class when one uses very inefficient number representations. The next example illustrates the construction. Example 9. Let Γ1 be the CRG defined in (Wooldridge and Dunne 2006, Example 1) where Ag = {a1, a2, a3}, G = {g1, g2}, R = {r1, r2}, the goals are given by Ga1 = {g1} Ga2 = {g2} Ga3 = {g1, g2} , the endowment function is en(a1, r1) = 2 en(a1, r2) = 0 en(a2, r1) = 0 en(a2, r2) = 1 en(a3, r1) = 1 en(a3, r2) = 2 ,

and the requirement function is req(g1, r1) = 3 req(g1, r2) = 2 req(g2, r1) = 2 req(g2, r2) = 1 .

The RCRG ΓR 1 is thus defined with Ag R = {a1, a2, a3}, GR = {pg1, pg1, pg1, pg2, pg2, pg2} with individual goals GR a1 = {pg1}, GR a2 = {pg2}, and GR a3 = {pg1, pg2}, and the endowment function is:

en R a1 = {pr1, pr1} {ρg1 pg1, ρg2 pg2} en R a2 = {pr2} {ρg1 pg1, ρg2 pg2} en R a3 = {pr1, pr2, pr2} {ρg1 pg1, ρg2 pg2} ,

where ρg1 = pr1 pr1 pr1 pr2 pr2 and ρg2 = pr1 pr1 pr2. In (Wooldridge and Dunne 2006), the authors study the relationship between CRG and Qualitative Coalitional Games (QCG) from (Wooldridge and Dunne 2004). A CRG and a QCG are said to be equivalent if the agents and the goals correspond, and there is a correspondence between the feasible sets of goals. We use the point of comparison here. We show that for every CRG Γ, there is a correspondence between the feasible sets of goals in Γ and in the RCRG ΓR obtained by the previous construction. Proposition 10. Let Γ = (Ag, G, R, (Gi)i Ag, en, req) be a CRG. For every coalition C Ag and every set of goals H G, we have

H feasΓ(C) iff

g H {pg} feasΓR(C) .

Proof. (sketch) We omit the proof of the right to left direction. From left to right. We build the RCRG ΓR = (Ag R, GR, (GR i )i Ag R, en R). Let C = {c1, . . . , c C}. Suppose H feasΓ(C). It means that r R, req(H, r) en(C, r). To achieve H, the contribution of agent i C in terms of the resource r R is the natural number κH(i, r) en(i, r). W.l.o.g., we assume that these contributions are optimal in the sense that for every resource r R, we have i C κH(i, r) = req(H, r).2

We must show that Ec1 en R c1, . . . , Ec C en R c C such that Ec1, . . . , Ec C H. When i C and i = c C, we define: Ei =

r R {pr, . . . , pr κH(i,r)

We also define:

r R {pr, . . . , pr κH(c C,r)

g H {ρg pg}

It is routine to check that the conditions are met. For every i C, we have indeed that Ei en R i . We can always build a formal proof of Ec1, . . . , Ec C H, which uses exclusively the rules (ax), ( R), ( L), and (E). (Example 11 presents such a proof on a specific case.)

2This assumption is necessary only if LOG is not affine. Otherwise, we can take care of the extra resources provided by agents by applying weakening.

Example 11. In the CRG Γ1 defined in Example 9, we have {g2} feasΓ1({a1, a2}). By Prop. 10, it must be that in the RCRG ΓR 1 , we have {pg2} feasΓR({a1, a2}). We show that it is indeed the case. Let Ea1 = {pr1, pr1} en R a1 and Ea2 = {pr2, (pr1 pr1 pr2) pg2} en R a2. We can formally demonstrate that Ea1, Ea2 pg2.

ax pr2 pr2 R pr1, pr2 pr1 pr2 R pr1, pr1, pr2 pr1 pr1 pr2

ax pg2 pg2 L pr1, pr1, pr2, (pr1 pr1 pr2) pg2 pg2

Winning coalitions Let Γ be an RCRG, and C a non-empty coalition. We say C is winning when sf Γ(C) = , and that it is losing otherwise. We assume that the empty coalition is losing. When C is winning in Γ, we also say that the value of coalition C is 1, written VALΓ(C) = 1. When C is losing, we say that the value of coalition C is 0, written VALΓ(C) = 0. An RCRG Γ associated with the valuation function VALΓ is thus effectively a simple game.

Example 12. Let Γ be the RCRG ({1, 2, 3}, {A, A A}, G1 = {A}, G2 = {A A}, G3 = {A}, en1 = {A}, en2 = {A}, en3 = {A, A}). (Assume that A, and A A are not provably equivalent to the vacuous resource 1, in which case all non-empty coalitions are winning.)

C {1, 2, 3} VALΓ(C)

0 {1} 1 {2} 0 {3} 1 {1, 2} 0 {1, 3} 1 {2, 3} 1 {1, 2, 3} 1

It is indeed a simple example, and it admits simple proofs involving only the rules (ax) and ( R). We see that VALΓ({2, 3}) = 1. So {2, 3} is a winning coalition. To see it, take E2 = en2 = {A}, and E3 = en3 = {A, A}. We can prove that E2, E3 (A A) A, as follows:

ax A A ax A A R A, A A A ax A A R A, A, A (A A) A Remark 13. RCRGs are in general neither monotonic nor superadditive. The former may be unusual, while the latter is particularly expected for a class of simple games. In general, RCRGs are not monotonic. In Example 12 we can see that VALΓ({1}) = 1, but VALΓ({1, 2}) = 0. In general, RCRGs are not superadditive. In Example 12 we can see that VALΓ({1}) = 1 and VALΓ({3}) = 1, but VALΓ({1, 3}) = 1 < VALΓ({1}) + VALΓ({3}).

The problem WIN is defined as follows.

Definition 14. Let Γ be an RCRG. WIN: Given a coalition C Ag, answer to the question VALΓ(C) = 1? .

In (Wooldridge and Dunne 2004), it is shown that WIN (called SUCCESSFUL COALITION there) is NPcomplete for CRGs. In this section, we prove the results summarized in Table 1 The correctness of Algorithm 1 for WIN is immediate from the definitions. The complexity follows from a simple

Algorithm 1 Non deterministic algorithm for WIN

IN: an RCRG Γ = (Ag, G, (Gi)i Ag, en), a coalition C = {c1, . . . , c C} Ag OUT: true if C is winning, false otherwise 1: non-deterministically guess (H, E, gc1, . . . , gc C) G en C Gc1 . . . Gc C. 2: return (

i C{gi} H) and (E H).

analysis and the fact that the line 2 can be evaluated in polynomial space when LOG is MALL and in non-deterministic polynomial time when LOG is MLL (Lincoln et al. 1992). Since NPNP = Σp 2 and NPPSPACE = PSPACE, we obtain:

Proposition 15. WIN is in Σp 2 for MLL RCRGs, and in PSPACE for MALL RCRGs.

Finally, we consider the case of affine RCRGs, for which we are able to provide tight complexity results for the WIN problem. There is a polynomial-time many-one reduction from instances of the problem of sequent validity for affine LOG, into instances of the problem of WIN for affine RCRG.

Proposition 16. WIN for affine RCRGs is as hard as sequent validity in the underlying logic LOG.

Proof. By applying the rules ( L) and ( R), A1, . . . , An B1, . . . , Bm iff A1, . . . , An, B2, . . . , Bm B1 is immediate. Thus, w.l.o.g., we can restrict our attention to intuitionistic sequents, of the form A1, . . . , An B. From such a sequent, we construct the (one-goal) affine RCRG Γ = (Ag, G, (Gi)i Ag, en) as follows. Ag = {a}; G = {B}; Ga = {B}; ena = {A1, . . . , An}. We want to show that A1, . . . , An B is valid iff sf Γ({a}) = . From left to right. Let H = {B} G. Clearly B Ga and {B} H. So, H satΓ({a}). Now, suppose A1, . . . , An B. Since {A1, . . . , An} ena, we clearly have that H feasΓ({a}). So H satΓ({a}) feasΓ({a}), and sf Γ({a}) = . From right to left. Suppose sf Γ({a}) = . It means that H satΓ({a}) feasΓ({a}). By definition of satΓ and Ga, necessarily H = {B}. By definition of feasΓ, Ea {A1, . . . , An} such that Ea B. Since Γ is affine, by rule (W), we can add to the left of the sequent every formula in {A1, . . . , An}\Ea, and obtain that A1, . . . , An B.

For one-goal affine RCRGs, we can reduce the problem of WIN for one-goal affine RCRGs to the problem of sequent validity in the affine LOG. This is stated by the following lemma.

Lemma 17. Let Γ = (Ag, G, ({gi})i Ag, en) be a one-goal affine RCRG, and let C Ag be a coalition. sf Γ(C) = iff en C

Proof. Right to left is immediate. For left to right, suppose sf Γ(C) = . Since the RCRG is one-goal, there is only one way to satisfy the goals of all the players: H satΓ(C) only if gi H for all players i C. So E en C such that E i C gi. Since the RCRG is affine, we can use rule (W). We apply it by adding successively to the left of the sequent every formula in en C \E (respecting the multiplicities). We finally obtain en C

i C gi by applying rule (E) enough times.

From Lemma 17 and Proposition 16, we obtain the following result. Proposition 18. WIN is NP-complete for one-goal affine MLL RCRGs and PSPACE-complete for one-goal affine MALL RCRGs. The problem WIN is central, and instrumental for other problems, some of which we study the next section.

The core of one-goal affine RCRGs When studying the powers of coalitions, there are at least two remarkable types of players: dummy and veto. RCRG are simple games, and in simple games, Player i is a veto player when there is no winning coalition without Player i s contribution. Let Γ = (Ag, G, (Gi)i Ag, en) be an RCRG. Player i is a veto player iff for every coalition C Ag, if C is a winning coalition, then i C. On the other hand, Player i is a dummy player when its presence or absence in a coalition does not change the value; it has neither a positive nor a negative impact. Player i is a dummy player iff for every coalition C Ag we have VALΓ(C {i}) = VALΓ(C). A payoff vector specifies how the gains of the grand coalition are distributed among the players. A payoff vector is a tuple p = (p1, . . . , pn) Rn 0 such that i Ag pi =

VALΓ(Ag). The value pi denotes the payoff of agent i. The payoff of coalition C Ag is defined as p C = i C pi. If the value of a coalition is strictly greater than its payoff from p, its members have an incentive to break from the grand coalition and work together to achieve its actual value; we say the coalition blocks p. The coalition C blocks the payoff vector p iff p C < VALΓ(C). The core of a game is an important solution concept. Definition 19. Let Γ = (Ag, G, (Gi)i Ag, en) be an RCRG. The core is the set of payoff vectors that are not blocked by any coalition. In this section, we study the following problems. Definition 20. Let Γ = (Ag, G, (Gi)i Ag, en) be an RCRG. VETO: Given a player i Ag, answer the question is i a veto player? . DUMMY: Given a player i Ag, answer the question is i a dummy player? . CNE: Answer the question is the core non-empty? . From now on, we shall concentrate on one-goal affine RCRGs. We prove the results summarized in Table 2 and Table 3.

VETO Given an RCRG Γ, and a player i, deciding VETO is done by checking that Player i is a member of all winning coalitions: C Ag, if VALΓ(C) = 1 then i C.

Class of RCRG WIN

MLL in Σp 2 (Prop. 15) MALL in PSPACE (Prop. 15) Affine MALL PSPACE-complete (Prop. 15, Prop. 16) One-goal affine MLL NP-complete (Prop. 18) One-goal affine MALL PSPACE-complete (Prop. 18)

Table 1: Complexity of WIN

Class of RCRG VETO DUMMY CNE

One-goal affine MLL in Πp 2 (Prop. 21) in Πp 2 (Prop. 23) in Δp 3 (Prop. 28) One-goal affine MALL in PSPACE (Prop. 21) in PSPACE (Prop. 23) in PSPACE (Prop. 28)

Table 2: Complexity upper-bounds of VETO, DUMMY, and CNE in one-goal affine RCRGs

Algorithm 2 Non deterministic algorithm for co VETO

IN: an RCRG Γ = (Ag, G, (Gi), en), a player i Ag OUT: true if i is not a veto player in Γ, false otherwise 1: non-deterministically guess C Ag \ {i}. 2: return C is winning? .

The complexity membership of VETO follows from a simple analysis of Algorithm 2, together with Proposition 18. Proposition 21. In one-goal RCRGs, VETO is in Πp 2 when LOG is affine MLL, and in PSPACE when LOG is affine MALL. We show that deciding VETO for a class C of RCRG is as hard as deciding co WIN in one-goal C. Proposition 22. In one-goal RCRGs, VETO is co WINhard.

Proof. (sketch) Let Γ = (Ag, G, (Gi)i Ag, en) be a one-goal RCRG and let C Ag be a coalition. We build the 2-player one-goal RCRG Γ = ({a, b}, {ga, gb}, (ga, gb), (ena, enb)) where ga = 1, ena = , gb =

i C gi, enb = en C. We can show that C is winning in Γ iff Player a is not a veto player in Γ .

Algorithm 3 Non deterministic algorithm for co DUMMY

IN: an RCRG Γ = (Ag, G, (Gi), en), a player i Ag OUT: true if i is not a veto player, false otherwise 1: non-deterministically guess C Ag. 2: win C := C is winning? 3: win C\i := C \ {i} is winning? 4: return (win C and not win C\i) or (not win C and win C\i) .

We can employ Algorithm 3. Together with Proposition 18, its analysis yields the following result.

Proposition 23. In one-goal RCRGs, DUMMY is in Πp 2 when LOG is affine MLL, and in PSPACE when LOG is affine MALL.

We show that deciding DUMMY for a class C of RCRG is as hard as deciding co WIN in one-goal C.

Proposition 24. In one-goal RCRGs, DUMMY is co WINhard.

Proof. (sketch) Let Γ = (Ag, G, (Gi)i Ag, en) be a onegoal RCRG and let C Ag be a coalition. We build the 1player one-goal RCRG Γ = ({a}, {ga}, (ga), (ena)) where ga =

i C gi, and ena = en C. We can show that C is winning in Γ iff Player a is not a dummy player in Γ .

We characterise the existence of an imputation in the core through three lemmas. When the grand coalition Ag is winning, CNE depends on the existence of a veto player.

Lemma 25. If the grand coalition is winning, then the core of an RCRG is non-empty iff there is a veto player.

Proof. (sketch) Assume VALΓ(Ag) = 1. We only show the left to right direction. Let p = (p1, . . . , pn) be a payoff vector in the core. By definition, it is not blocked by any coalition: for all C Ag, we have p C =

i C pi VALΓ(C). Now pick v Ag, such that pv > 0 (such a player exists because Ag is winning and p Ag = VALΓ(Ag) = 1). We show that v is a veto player. Let C be an arbitrary coalition such that v C. Since v C and pv > 0, we have p C < p Ag = v(Ag) = 1. Moreover, like all coalitions, C does not block p, so VALΓ(C) p C. We thus have v(C) < 1, and since RCRG are simple games, v(C) = 0.

When the grand coalition Ag is losing, CNE depends on the absence of a winning coalition.

Lemma 26. If the grand coalition is losing, then the core of an RCRG is non-empty iff there is no winning coalition.

VETO DUMMY CNE

co WIN-hard (Prop. 22) co WIN-hard (Prop. 24) co WIN-hard (Prop. 29)

Table 3: Complexity lower-bounds of VETO, DUMMY, and CNE in every class of one-goal RCRGs

Proof. Assume VALΓ(Ag) = 0. Left to right. Let p = (p1, . . . , pn) be a payoff vector in the core. Since VALΓ(Ag) = 0 (Ag is losing), also p Ag = 0. Since p is in the core, it is not blocked by any coalition. For any coalition C, we have p C p Ag = 0. So p C = 0. It means that for all C Ag, we have 0 VALΓ(C). That is, VALΓ(C) = 0 for all coalitions C. Right to left. Suppose there are no winning coalitions. Let p be the payoff vector such that pi = 0 for all i Ag. We have p C = 0 = VALΓ(C) for every coalition C. So p is not blocked by any coalition and it is in the core.

This would be enough to propose a working algorithm. But we can aim for an arguably cleaner algorithm, justified by the following simple lemma.

Lemma 27. If the grand coalition is losing, then there is no winning coalition iff all players are dummies.

Proof. Assume VALΓ(Ag) = 0. Left to right. Suppose VALΓ(C) = 0 for all C Ag. So obviously, for every i Ag and for every C Ag, we have VALΓ(C {i}) = VALΓ(C). So all players are dummy. Right to left. Suppose that for every i Ag and for every C Ag, we have VALΓ(C {i}) = VALΓ(C). Now, let I Ag be an arbitrary coalition. We can show that I is losing. Let J = Ag \ I = {j1, . . . , jk}. A series of equalities follows: VALΓ(Ag) = VALΓ(Ag \ {j1}) = VALΓ(Ag \ {j1, j2}) = . . . = VALΓ(Ag \ {j1, j2, . . . , jk}) = VALΓ(I). By hypothesis VALΓ(Ag) = 0. We conclude that VALΓ(I) = 0.

Lemma 25, and Lemma 26 together with Lemma 27 ensure the correctness of Algorithm 4 to decide CNE. A con-

Algorithm 4 Algorithm for CNE

IN: an RCRG Γ = (Ag, G, (Gi)i Ag, en) OUT: true if the core of Γ is non-empty, false otherwise 1: if (Ag is winning): 2: for (i Ag): 3: if (i is a veto player): 4: return true. 5: return false. 6: else: 7: for (i Ag): 8: if (i is not a dummy player): 9: return false. 10: return true.

taining class of complexity for the problem CNE can be established by a simple analysis of the algorithm, together with the complexity of WIN (Prop. 18), VETO (Prop. 21), and DUMMY (Prop. 23).

Proposition 28. In one-goal RCRGs, CNE is in Δp 3 when LOG is affine MLL, and in PSPACE when LOG is affine MALL.

We show that deciding CNE for a class C of RCRG is as hard as deciding co WIN in one-goal C.

Proposition 29. In one-goal RCRGs, CNE is co WIN-hard.

Proof. (sketch) Let Γ = (Ag, G, (Gi)i Ag, en) be a one-goal RCRG and let C Ag be a coalition. We build the 2-player one-goal RCRG Γ = ({a}, {ga, gb}, (ga, gb), (ena, enb)) where ga =

i C gi, gb = X, ena = en C, enb = , and X is a fresh atomic proposition (not provably equivalent to 1). We can show that C is not winning in Γ iff the core of Γ is non-empty.

Formalization of Example 1 We formalise Example 1: b stands for bacon, e for one egg, and o for an omelet. Player 1 is happy with b, Player 2 is happy with either b or e (i.e., b e), and Player 3 is happy with o. Player 1 is endowed with one token of e and the consumable capacity of transforming an e into a o (i.e., e o). Player 2 is endowed with one token of b. Player 3 is endowed with one token of e. To formalise it, let Γ = (Ag, G, (Gi)i Ag, en) be the RCRG, where:

Ag = {1, 2, 3} G = {b, b e, o} G1 = {b} G2 = {b e} G3 = {o} en1 = {e, e o} en2 = {b} en3 = {e}

The winning coalitions are {2}, {1, 2}, and {1, 2, 3}. The coalition {2} is winning because b b e and {b} en2. The coalition {1, 2} is winning because e, b b (b e), {e} en1, and {b} en2. We show in more details that {1, 2, 3} is a winning coalition, and that they can win by using all their endowed resources. Specifically, en1, en2, en3 b (b e) o.

ax e e R e b e

ax e e ax o o L e o, e o R e, e o, e (b e) o R b, e, e o, e b (b e) o

def en1, en2, en3 b (b e) o

Since we have identified all the winning coalitions in Γ, we can easily determine the veto players. Player 2 is the only veto player of the game. Player 1 and Player 3 are not, as witnessed by {2} being a winning coalition. Player 3 is the only dummy player of the game Γ. Player 1 is not a dummy because VALΓ({1, 2, 3}) = 1 and VALΓ({2, 3}) = 0. Player 2 is not a dummy because VALΓ( ) = 0 and VALΓ({2}) = 1.

Let p = (0, 1, 0) be a payoff vector. It is in the core of the game. An analysis of the (left to right) proof of Lemma 25 indicates that it is the only one.

Discussion We have presented a simple, compact, and rich model of interaction for resource-conscious agents. In RCRGs, resources and goals are the same type of objects: LOG formulas. Resources can then be combined and transformed following the rules of LOG so as to yield goals. We proved with Prop. 10 that RCRGs generalise the CRGs presented in (Wooldridge and Dunne 2006), the same way that Qualitative Coalitional Games (QCG) (Wooldridge and Dunne 2004) generalise CRGs. QCGs and RCRGs on the other hand, seem to be incomparable. At least, they do not seem to have a natural formal relationship. QCGs are not compact, and rely on a characteristic function to represent the choices of the players. We could modify (extend) the RCRGs by adding such a characteristic function which would thus be an explicit representation of the choices (subsets of formulas) available to the players. Using classical logic in place of LOG, this would be sufficient to embed QCGs. The problem WIN for CRG is NP-complete (Wooldridge and Dunne 2006). We have proved that WIN is in Σp 2 for MLL RCRGs (Prop. 15), but only have shown it to be NPhard (Prop. 16) when the logic is affine. When we restrict our attention to the class of one-goal affine MLL RCRGs, the problem is NP-complete (Prop. 18). It will be interesting to determine whether WIN is in NP for MLL RCRGs. The problem WIN is central, and instrumental for other problems. We have studied VETO, DUMMY, and CNE. The core of CRGs was also studied in (Dunne et al. 2010) but by considering CRGs as non-transferable utility games. We instead, as in Coalitional Skill Games (CSGs) (Bachrach and Rosenschein 2008), considered RCRGs as transferable utility games. In CSGs, the problem CNE is in P for all the variants for which complexity results have been obtained (Bachrach and Rosenschein 2008). For one-goal MLL RCRGs, we proved that CNE is in Δp 3 (Prop. 28) capitalizing on auxiliary algorithms for WIN, VETO, and DUMMY. We only showed, however, that the problem is co NP-hard (co WIN-hard) in Prop. 29. More work is needed in this direction. We also have tight complexity results. Combining the results obtained in this paper, we have that:

Theorem 30. In one-goal affine MALL RCRG, VETO, DUMMY, and CNE are PSPACE-complete problems.

We have concentrated on one-goal affine RCRG for the algorithmic analysis of the core. Lemma 17 and Proposition 16 indicate that in the case of one-goal affine RCRGs, the problem WIN and the problem of sequent validity are inter-reducible. Our examples demonstrate that the class is already capable of representing intricate scenarios. In fact, multi-goals can be captured in one-goal MALL RCRGs using the operands and &: see Remark 7 and our formalization of Example 1. For non affine RCRGs, we can provide some results, but of questionable significance. We know that WIN is in Σp 2

for (arbitrary) MLL RCRGs (Prop. 15). Plugging it into the algorithms that we have provided, all we can say for now is that for arbitrary MLL RCRGs, VETO and DUMMY are in Πp 3 and CNE is in Δp 4. No hardness results were attained.

References Bachrach, Y., and Rosenschein, J. S. 2008. Coalitional skill games. In 7th International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 08, 1023 1030. International Foundation for Autonomous Agents and Multiagent Systems. De Young, H., and Sch urmann, C. 2012. Linear logical voting protocols. In E-Voting and Identity - Third International Conference, Vote ID 2011, Tallinn, Estonia, September 2830, 2011, Revised Selected Papers, volume 7187 of Lecture Notes in Computer Science, 53 70. Springer. Dunne, P. E.; Kraus, S.; Manisterski, E.; and Wooldridge, M. 2010. Solving coalitional resource games. Artificial Intelligence 174(1):20 50. Gabbay, D. M., and de Queiroz, R. J. G. B. 1992. Extending the curry-howard interpretation to linear, relevant and other resource logics. J. Symb. Log. 57(4):1319 1365. Girard, J.-Y. 1987. Linear logic. Theoretical Computer Science 50(1):1 101. Kanovich, M. I. 1994. The complexity of Horn fragments of Linear Logic. Annals of Pure and Applied Logic 69(2-3):195 241. Lincoln, P.; Mitchell, J.; Scedrov, A.; and Shankar, N. 1992. Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56(1-3):239 311. O Hearn, P. W., and Pym, D. J. 1999. The logic of Bunched Implications. Bulletin of Symbolic Logic 5(2):215 244. Porello, D., and Endriss, U. 2010a. Modelling combinatorial auctions in linear logic. In Lin, F.; Sattler, U.; and Truszczynski, M., eds., Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference, KR 2010. AAAI Press. Porello, D., and Endriss, U. 2010b. Modelling multilateral negotiation in linear logic. In ECAI 2010 - 19th European Conference on Artificial Intelligence, Proceedings, volume 215 of Frontiers in Artificial Intelligence and Applications, 381 386. IOS Press. Troelstra, A. S. 1992. Lectures on Linear Logic. CSLI Publications. Troquard, N. 2016. Nash equilibria and their elimination in resource games. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, 503 509. Wooldridge, M., and Dunne, P. E. 2004. On the computational complexity of qualitative coalitional games. Artificial Intelligence 158(1):27 73. Wooldridge, M., and Dunne, P. E. 2006. On the computational complexity of coalitional resource games. Artificial Intelligence 170(10):835 871.