Budget-Constrained Coalition Strategies with Discounting

1 Introduction

Several logical systems for reasoning about agent and coalition power in game-like settings have been previously proposed. Among them are coalition logics [Pauly, 2001; 2002], ATL [Alur et al., 2002], ATEL [van der Hoek and Wooldridge, 2003], ATLES [Walther et al., 2007], know-how logics [ ˚Agotnes and Alechina, 2019; Wang, 2018; Naumov and Tao, 2017; Fervari et al., 2017; Naumov and Tao, 2018b; 2018a; 2019], and STIT [Belnap and Perloff, 1990; Xu, 1995; Horty, 2001]. Some of these systems have been extended to incorporate resources and costs of actions [Alechina et al., 2011; Cao and Naumov, 2020; Alechina et al., 2011; Cao and Naumov, 2017; Alechina and Logan, 2018; Alechina et al., 2016; Della Monica et al., 2011; Alechina et al., 2017; 2015]. Even in the case of multi-step actions, these systems treat current and future costs equally.

At the same time, in game theory, accounting, and machine learning, costs of multi-step transitions are often discounted to reflect the fact that future costs and earnings have lesser present values. Thus, there is a gap between the way resources and costs currently are treated in logic and the way they are accounted for in other fields. To address this gap, in this paper we propose a sound and complete logic of coalition power whose semantics incorporates discounting. Although we formulate our work in terms of cost, it could be applied to any other resource measured in real numbers. It can also be straightforwardly extended to vectors of real numbers to incorporate multiple resources.

As an example, consider a single-player game depicted in Figure 1. This game has four game states w, u, v, and s and a single terminal state t. Propositional variable p is true in game states w, u, and v and is false in game state s. We assume that the values of propositional variables are not defined in the terminal state t. The agent a has multiple actions in each game state. These actions are depicted in Figure 1 using directed edges. The cost of each action to agent a is shown as a label on the directed edge. For instance, the directed edge from state w to state u with label 2 means that the agent a has an action with cost 2 to transition the game from state w to state u. Transitioning to the terminal state t represents the termination of the game.

Note that in state w the agent has two strategies to maintain condition p indefinitely. The first strategy consists of transitioning the game to state u at cost 2 and then repeatedly applying the action with cost 2 to keep the game in state u. Without discounting, the cost of this strategy is 2 + 2 + 2 + · · · = +∞. The agent also has another strategy to maintain condition p that consists in transitioning to state v at cost 1 and then keeping the game in state v with recurrent cost 1. Intuitively, the second strategy is less expensive than the first because each step costs half as much. However, formally, the cost of the second strategy without discounting is the same as the first one: 1 + 1 + 1 + · · · = +∞.

The problem that we observe here is not specific to costs of strategies. A similar situation also appears in repetitive games, accounting, and reinforcement machine learning algorithms based on Markov decision processes. The solution commonly used to resolve this problem is discounting. It consists of counting the cost on the first step at nominal value, the cost on the second step with a discount factor γ ∈ (0, 1), the cost on the third step with discount factor γ 2 , etc. With discounting, the total cost of our first strategy is

while the cost of our second strategy is

Since 1 1-γ < 2 1-γ , we can say that with discounting the second strategy is less expensive than the first. In the rest of this paper, we assume a fixed discount factor γ ∈ (0, 1).

2 Outline

The rest of this paper is structured as follows: In the next section, we introduce a class of games that will later be used to define the semantics our logical system. Section 4 defines the language of our system. Section 5 gives the discountingbased semantics of this language. Section 6 shows that the properties of strategies with discounting depend on whether we consider strategies with or without perfect recall. Section 7 lists and discusses the axioms of our logical system for the strategies with perfect recall. Section 8 proves the completeness of our system. Section 9 concludes. Additionally, the proof of soundness can be found in the full version of this paper [Bozzone and Naumov, 2021].

3 Game Definition

Throughout the paper, we assume a fixed nonempty set of propositional variables and a fixed set of agents A. By a coalition we mean any subset of A. By XA we mean the set of all functions from set A to a set X.

The class of games that we consider is specified below.

Definition 1 A game is a tuple (W, t, ∆, ε,M, π), where

1. W is a set of game states,
2. t /∈ W is a terminal state, by W + we denote the set of all states W ∪ {t},
3. ∆ is an arbitrary set called domain of actions,
4. ε ∈ ∆ is a zero-cost action,
5. M ⊆ W × ∆A × [0,∞)A × W + is a relation called mechanism, such that
6. (a) for each tuple (w, δ, u,w′ ) ∈ M and each agent a ∈ A, if δ(a) = ε, then u(a) = 0,
7. (b) for each state w ∈ W and each complete action profile δ ∈ ∆A, there is a function u ∈ [0,+∞)A and a state w′ ∈ W + such that (w, δ, u, w′ ) ∈ M,
8. π is a valuation function that maps propositional variables into subsets of W.

Intuitively, mechanism is a set of all quadruples (w, δ, u, v) such that the game might transition from state w to state v under action profile δ at costs to the individual agents specified by function u.

The defined above games are similar to resource-bounded action frames, which are the semantics of Resource-Bounded Coalition Logic (RBCL) [Alechina et al., 2011]. In particular, both of them have a zero-cost action.

However, there are several differences between these two classes of models. Unlike RBCL frames, our games have only one resource that we call "cost". We do this for the sake of presentation simplicity. Multiple resources could be incorporated into our system without any significant changes to the results in this paper. RBCL allows only non-negative integer resource requirements, while costs in our games are nonnegative real numbers. RBCL assigns a unique cost to each action, while our games assign cost to each transition. As a result, the cost to the agent in our setting depends not only on the action of the agent but also on the actions of the other agents. This is similar to how the utility function of an agent in game theory is a function of the complete action profile, not just of the action of that agent. We achieve this by including the cost of the transition for each agent as the third component of a tuple from the mechanism relation.

Furthermore, the RBCL frames are deterministic while our games are not deterministic because we represent mechanism as a relation, not a function. Unlike RBCL frames, our games can be terminated by the agents. In order to make our semantics more general, the games are terminated through a transition to a terminal state. Such transitions allow the agents to be charged upon the termination of a game. This ability is significant for our proof of completeness.

The game depicted in Figure 1 has only one player. Figure 2 depicts a two-player game. Note that our general notion of the game captured in Definition 1 allows each agent to influence the outcome of each transition and imposes a cost for each transition on each agent. For the sake of simplicity, the game depicted in Figure 2 designates a single "dictator" agent in each state. For example, in state w, the dictator is agent a. The dictator is solely responsible for the choice of the next state and bears all the costs associated with the transition. In the diagram, the dictator is specified inside each state's circle. Note that in state w agent a has a strategy to maintain condition p at cost 100+100γ+100γ 2 +· · · = 100 1-γ to herself and cost 0 + 0γ + 0γ 2 + · · · = 0 to agent b.

Definition 2 A play in game (W, t,∆, ε,M, π) is a finite sequence w0, δ0, u0, w1, . . . , δn-1, un-1, wn such that

1. wi ∈ W for 0 ≤ i < n and wn ∈ W +,
2. δi ∈ ∆A, where 0 ≤ i < n,

1. ui ∈ [0,∞)A is a cost function, where 0 ≤ i < n,
2. (wi-1, δi-1, ui-1,wi) ∈M, where 1 ≤ i ≤ n.

The set of all plays of a given game is denoted by Play.

4 Syntax

The language Φ of our system is defined by the grammar

where p is a propositional variable, C is a coalition, and x is a "constraint" function from set C to [0,+∞). We read [C]xϕ as "coalition C has a strategy to maintain condition ϕ at individual cost no more than x(a) to each member a ∈ C".

If C is a coalition {a1, . . . , an} and x is a function from set C to [0,+∞) such that x(ai) = xi for each i ≤ n, then we will use shorthand notation [a1, . . . , an]x1,...,xn ϕ to refer to formula [C]xϕ.

Definition 3 For any real µ > 0 and any formula ϕ ∈ Φ, formula ϕ/µ is defined recursively as follows:

1. p/µ ≡ p, for any propositional variable p,
2. (¬ϕ)/µ ≡ ¬(ϕ/µ),
3. (ϕ→ψ)/µ ≡ (ϕ/µ) → (ψ/µ),
4. ([C]xϕ)/µ ≡ [C]x/µ(ϕ/µ).

For example, ([a, b]4,6¬[b, c]8,2 p)/2 = [a, b]2,3¬[b, c]4,1 p.

5 Semantics

In this section we define the semantics of our logical system.

Definition 4 An action profile of a coalition C is a function from set C to set ∆.

Definition 5 A strategy of a coalition C is a function from set C × P lay to set ∆.

Note that each strategy takes into account not just the current state but the whole play. Thus, the strategies that we consider are perfect recall strategies. We will discuss this in detail in the next section.

Definition 6 A play w0, δ0, u0,w1, . . . , un-1,wn ∈ Play satisfies strategy s of a coalition C if for each i such that 0 ≤ i < n and each agent a ∈ C,

For any functions x and y, we write x ≤C y if x(a) ≤ y(a) for each a ∈ C. We define notation x =C y similarly.

Definition 7 For each formula ϕ ∈ Φ and each state w ∈ W of a game (W, t,∆, ε,M, π), satisfaction relation w ⊩ ϕ is defined recursively as follows:

1. w ⊩ p, if w ∈ π(p),
2. w ⊩ ¬ϕ, if w ⊮ ϕ,
3. w ⊩ ϕ→ψ, if w ⊮ ϕ or w ⊩ ψ,
4. w ⊩ [C]xϕ if there is a strategy s of coalition C such that for any play w0, δ0, u0,w1, . . . , un-1,wn ∈ Play that satisfies strategy s, if w = w0, then
5. (a) ∑n-1 i=0 uiγ i ≤C x and
6. (b) if wn ̸= t, then wn ⊩ ϕ/γ n .

To understand why item 4(b) of the above definition uses formula ϕ/γ n instead of formula ϕ, let us consider an example of a formula ϕ ≡ [D]yψ. Note that formula [C]x[D]yψ states that coalition C can maintain at cost x the ability of coalition D to maintain ψ at cost y. Consider the hypothetical case where C, at cost x to C, will be maintaining this ability of D for, say, 10 transitions. The formula [C]x[D]yψ states that after 10 moves coalition D should be able to take over and maintain condition ψ at cost y to D. Given that in our setting the costs are discounted, an important question is whether y is measured in today's money or future money. Note that y in future money is yγ 10 in today's money. On the other hand, y in today's money is y/γ 10 in future money. In this paper we decided to measure all costs in today's money. Thus, cost y in [C]x[D]yψ refers to costs in today's money (in state w0 of Definition 7). In future money (in state wn), the same cost is y/γ n . As a result, item 4(b) of Definition 7 uses formula ϕ/γ n instead of just ϕ.

Consider again the game depicted in Figure 2. As discussed earlier, in state w, single-agent coalition {a} has a strategy to maintain condition p by looping in state w at recurrent cost 100. The total cost of this strategy is 100+100γ+ 100γ 2 + · · · = 100 1-γ . Thus, w ⊩ [a]100/(1-γ) p. In the same game, single-agent coalition {b} also has a strategy to maintain condition p. The strategy consists in pushing the game back to state w each time when agent a transitions the game out of state w either into state u or state v. The cost of the "pushing back" action from state u and v is 1 and 200 respectively. Hence, the total cost to agent b could be no more than 0 + 200γ + 0 + 200γ 3 + 0 + · · · = 200γ/(1 - γ 2 ). Then, w ⊩ [b]200γ/(1-γ 2 ) p. Finally, note that if agents a and b decide to cooperate, then maintaining condition p becomes significantly less expensive for both of them because they can alternate the state of the game between states w and u. The total cost of the joint strategy to agent a is 1+0+γ 2+0+γ 3+· · · = 1 1-γ 2 and to agent b is 0+γ+0+γ 3 +· · · = γ 1-γ 2 . Therefore,

6 Perfect Recall Assumption

Definition 5 specifies a strategy of a coalition as a function that assigns an action to each member of a coalition based on a play of the game. In other words, any strategy has access to the whole history of the game rather than just to the current state. Such strategies are often referred to as perfect recall strategies. As the next example shows, perfect recall strategies might have different discounted costs than memoryless strategies for the same condition to maintain in the same game.

Consider the game depicted in Figure 3 and assume, for this example only, that γ = 2/3. Suppose that coalition {a, b, d} wants to maintain condition p starting from state w1.

Since agent c is not a member of the coalition, the coalition has no control whether the system transitions from state w1 to state w2 or w3. Once the system is either in state w2 or state w3, in order to maintain the condition p, agent a or agent b, respectively, will have to transition the game to state w4 at cost 43 γ = 43 · 23 = 89 to the agent. In state w4, the coalition faces a choice between (i) transitioning game into state w5 in which agent a encounters cost

to maintain p and (ii) transitioning game into state w6 in which agent b encounters the same cost 1γ 3 +1γ 4 + · · · = 89 to maintain condition p.

If agent d has a perfect recall, then she can balance the costs between agents a and b by transitioning to state w6 if the game transitioned to w4 from state w2 and transitioning to state w5 if the game transitioned to w4 from state w3. This way, agents a and b encounter the same total costs 8/9:

At the same time, if agent d does not have memory about the previous state of the game, then either agent a or b might encounter a total cost as high as 8/9 + 8/9 = 16/9 while executing the coalition strategy to maintain condition p:

In this paper, we consider discounted costs under perfect recall assumption for all agents.

7 Axioms

In this section, we introduce a logical system describing the properties of coalition power modality [C]xϕ. In addition to propositional tautologies in language Φ, the system contains the following axioms:

1. Reflexivity: [C]xϕ→ϕ,
2. Cooperation: if C ∩D = ∅, then [C]x(ϕ → ψ) → ([D]yϕ → [C ∪ D]x∪yψ),
3. Monotonicity: [C]xϕ→ [C]yϕ, where x ≤C y,
4. Transitivity: [C]xϕ→ [C]x[C]xϕ.

Recall that the value of discount factor γ has been fixed at the end of Section 1. It is worth noting that this factor does not appear explicitly in any of the above axioms.

The Reflexivity axiom says that if coalition C can maintain condition ϕ at discounted cost x starting from the current state, then condition ϕ must be true in the current state. The Cooperation axiom states that if coalitions C and D are disjoint, coalition C can maintain condition ϕ → ψ at cost x, and D can maintain condition ϕ at cost y, then together they can maintain condition ψ at cost x∪y. Here, by x∪y we mean the union of two functions with disjoint domains. The Monotonicity axiom states that if a coalition can maintain condition at some cost, then it can maintain the same condition at any larger cost.

The assumption of the Transitivity axiom states that coalition C has a strategy, say s, to maintain condition ϕ at cost x in perpetuity. The conclusion states that the same coalition can, at cost x, maintain its own ability to maintain ϕ at cost x. To achieve this, coalition C can use the same strategy s. Indeed, assume that coalition C used strategy s for some number of steps at cost x′ ≤C x in today's money. Thus, it should be able to keep using it at cost x-x′ ≤C x in today's money to maintain ϕ. Note that it is crucial for this argument that all costs are computed in today's money. Furthermore, the Transitivity axiom is not sound if the cost in the internal modality is measured in future money. A non-trivial proof of soundness of the Transitivity axiom as well as the proofs soundness of all other axioms can be found in [Bozzone and Naumov, 2021].

We write ⊢ ϕ and say that formula ϕ is a theorem if ϕ is derivable from the above axioms using the Modus Ponens and the Necessitation inference rules:

In addition to unary relation ⊢ ϕ, we also consider binary relation X ⊢ ϕ. Let X ⊢ ϕ if formula ϕ is provable from the theorems of our logical system and the set of additional assumptions X using only the Modus Ponens inference rule. The proofs of the next three auxiliary lemmas can be found in [Bozzone and Naumov, 2021].

Lemma 1 If ϕ1, . . . , ϕn ⊢ ψ and sets C1,. . . ,Cn are pairwise disjoint, then

8 Completeness

In this section, we prove the completeness of our logical system. We start the proof by defining the canonical game (W, t,∆, ε,M, π). The set W is the set of all maximal consistent sets of formulae in language Φ, and t is an arbitrary element such that t /∈ W. Let ε be an arbitrary element such that ε /∈ Φ and the set of actions ∆ be Φ ∪ {ε}.

Definition 8 Mechanism M is the set of all quadruples (w, δ, u,w′ ) ∈ W × ∆A × [0,∞)A × W + such that if [C]xϕ ∈ w and δ(a) = [C]xϕ for each agent a ∈ C, then

Informally, action δ(a) = [C]xϕ of an agent a ∈ C means "as a part of coalition C, I request to maintain condition ϕ at individual cost x(b) to each member b ∈ C". In order for the request to be valid, it should be submitted by all members of coalition C. Even if all members of coalition C submit the request, it is enforced by the mechanism only if formula [C]xϕ belongs to the current state w. Condition 1 of Definition 8 stipulates that although the mechanism is free to set the cost u of the transition below what the members of the coalition offered to pay, the mechanism cannot overcharge them. If the mechanism decides to charge members of the coalition the amount u for transition to state w′ , then it also must provide the opportunity for the members to continue to maintain the condition ϕ at cost x - u. The latter is captured by condition 2 of Definition 8.

This concludes the definition of the canonical game (W, t,∆, ε,M, π). As usual, the key step in proving the completeness theorem is an "induction" (or "truth") lemma, which in our case is Lemma 6. Lemma 4 and Lemma 5 below are two auxiliary lemmas that capture the two directions of the induction lemma in the case when formula ϕ has the form [C]xψ.

Lemma 4 For each state w ∈ W + and each formula [C]xϕ ∈ w, there is strategy s of coalition C such that, for each play w0, δ0, u0, w1, . . . , un-1, wn satisfying strategy s, if w = w0, then

1. ∑n-1 i=0 uiγ i ≤C x and
2. if wn ̸= t, then ϕ/γ n ∈ wn.

PROOF. Let action s(a, λ) for any agent a ∈ C and any play λ = w0, δ0, u0, w1, . . . , un-1, wn be defined 1 as follows:

where z = ∑n-1 i=0 uiγ i .

Consider an arbitrary play w0, δ0, u0,w1, . . . , un-1,wn satisfying strategy s such that w = w0. It will be sufficient to show that conditions 1 and 2 of the lemma hold for this play.

Claim 1 For each a ∈ C and each k such that 0 ≤ k ≤ n,

1. ∑k-1 i=0 uiγ i ≤C x,

PROOF OF CLAIM. We prove the claim by induction on integer k. If k = 0, then ∑k-1 i=0 uiγ i = 0 ≤C x by the definition of language Φ because [C]xϕ is a formula. Also,

by the assumption [C]xϕ ∈ w of the lemma and the assumption w = w0.

1 Informally, strategy s always requests to maintain condition ϕ using remaining budget x - z.

Suppose k > 0. Then, (wk-1, δk-1, uk-1,wk) ∈ M by Definition 2, the assumption of the lemma that w0, δ0, u0, w1, . . . , un-1, wn is a play, and the assumption of the claim that k ≤ n. Thus, wk-1 ̸= t by item 5 of Definition 1. Hence, by the induction hypothesis,

By Definition 6 (step i), equation (2) and equation (1) (step ii), and item 4 of Definition 3 (step iii),

At the same time, by item 4 of Definition 3 (step iv) and equation (3) (step v),

Also, (wk-1, δk-1, uk-1, wk) ∈ M by Definition 2 and the assumption that w0, δ0, u0, w1, . . . , un-1, wn is a play. Thus, by Definition 8 and statements (5) and (4),

Thus, by the laws of algebra and item 4 of Definition 3,

The last two statements imply, respectively, parts 1 and 2 of the claim. ⊠

The statement of the lemma follows from the above claim when k = n. The first part follows immediately. To show the second part, note that by Definition 3, item 2 of the claim implies ([C](x-∑n-1 i=0 uiγ i )/γn(ϕ/γ n )) ∈ wn. Thus, wn ⊢ ϕ/γ n by the Reflexivity axiom and the Modus Ponens inference rule. Therefore, ϕ/γ n ∈ wn because set wn is maximal. ⊠

Lemma 5 For each state w ∈ W, each formula [C]xϕ /∈ w, and each action profile α of coalition C, there is a complete action profile δ, a cost function u ∈ [0,+∞)A, and a state w′ ∈ W + such that α =C δ, (w, δ, u,w′ ) ∈ M, and either (i) u ̸≤C x or (ii) w′ ̸= t and ϕ/γ /∈ w′ .

PROOF. Define the complete action profile

and cost function 2

Note that α =C δ. We consider the following two cases: Case I: u(a) = 0 for each agent a ∈ C. Define set X to be

Claim 2 Set X is consistent.

PROOF OF CLAIM. Suppose set X is not consistent. Thus, there are formulae

such that

and

Without loss of generality, we can assume that formulae ([D1]y1 ψ1)/γ, . . . , ([Dn]yn ψn)/γ are distinct. Thus, formulae [D1]y1 ψ1, . . . , [Dn]yn ψn are also distinct by Definition 3. Hence, sets D1, . . . ,Dn are pairwise disjoint due to assumption (9).

By Lemma 2, statement (10) implies that

Then, by Lemma 1 and because sets D1, . . . , Dn are pairwise disjoint,

Thus, by the Transitivity axiom and the Modus Ponens inference rule applied n times,

Notice that yi(a) ≤ x(a) for any i ≤ n and any agent a ∈ Di. Indeed, suppose that yi(a) > x(a). Hence u(a) = yi(a) by the choice of cost function u and statements (8) and (9). Thus, u(a) > x(a). Then, u(a) > 0 because function x is nonnegative by the assumption [C]xϕ ∈ Φ, which contradicts the assumption u(a) = 0 of the case. Hence, by Lemma 3 and the Modus Ponens inference rule,

2 The choice of function u is perhaps the most unexpected step in our proof. Informally, if agent a is "bluffing" and is offering to pay more than x(a), then function u charges the agent the amount she offered to pay, y(a). If the agent makes a "modest" offer of no more than x(a), then she is not charged at all.

Then, w ⊢ [C]xϕ by the assumption (7). Thus, [C]xϕ ∈ w because set w is maximal, which contradicts the assumption [C]xϕ /∈ w of the lemma. ⊠

Let w′ be any maximal consistent extension of set X. Note that ¬(ϕ/γ) ∈ X ⊆ w′ by the choice of sets X and w′ . Thus, ϕ/γ /∈ w′ because set w′ is consistent.

Claim 3 (w, δ, u,w′ ) ∈M.

PROOF OF CLAIM. Consider any formula [D]yψ ∈ w such that

By Definition 8, it suffices to show that u ≤D y and ([D]y-uψ)/γ ∈ w′ . We consider the following two cases:

Case Ia: D ⊆ C. Thus, α(a) = δ(a) = [D]yψ for each agent a ∈ D by equation (6) and assumption (11). Hence, ([D]yψ)/γ ∈ X by the choice of set X. Then, ([D]y-uψ)/γ ∈ X by the assumption of Case I that u =C 0 and the assumption D ⊆ C of Case Ia. Therefore, ([D]y-uψ)/γ ∈ w′ by the choice of set w′ . Additionally, u =D 0 ≤D y because 0 ≤D y by the definition of Φ.

Case Ib: There is an agent a ∈ D \ C. Hence, ⊤ = δ(a) = [D]yψ by equation (6) and assumption (11). Therefore, formula [D]yψ is identical to formula ⊤, which is a contradiction. ⊠

Note that ¬(ϕ/γ) ∈ X ⊆ w′ by the choice of sets X and w′ . Therefore, ϕ/γ /∈ w′ because set w′ is consistent.

Case II: u(a) ̸= 0 for at least one agent a ∈ C. Thus, u(a) = y(a) > x(a) by the choice of function u. Therefore, u ̸≤C x. Choose w′ to be the terminal state t.

Claim 4 (w, δ, u,w′ ) ∈M.

PROOF OF CLAIM. Consider any formula [D]yψ ∈ w such δ(a) = [D]yψ for each agent a ∈ D. By Definition 8 and because w′ = t, it suffices to show that u ≤D y. Recall that 0 ≤D y because [D]yψ is a formula. Therefore, u ≤D y by the choice of function u. ⊠

This concludes the proof of the lemma. ⊠

The next lemma is usually referred to as an "induction" or "truth" lemma. It is proven by induction on the structural complexity of formula ϕ using Lemma 4 and Lemma 5 in the case where formula ϕ has the form [C]xψ. The proof of this lemma can be found in [Bozzone and Naumov, 2021].

Lemma 6 w ⊩ ϕ iff ϕ ∈ w for each state w ∈ W and each formula ϕ ∈ Φ.

Theorem 1 If X ⊬ ϕ, then there is a state w of a game such that w ⊩ χ for each χ ∈ X and w ⊮ ϕ.

PROOF. Suppose that X ⊬ ϕ. Let w be any maximal consistent extension of set X ∪ {¬ϕ}. Note that w is a state of the canonical game. Then, w ⊩ χ for each χ ∈ X and w ⊩ ¬ϕ by Lemma 6. Therefore, w ⊮ ϕ by Definition 7. ⊠

9 Conclusion

In this paper we proposed a coalition power logic whose semantics incorporates discounting. The main technical result is a strongly sound and strongly complete logical system for coalition strategies with perfect recall.