A Logic for Coalitions with Bounded Resources

1 Introduction

Recent work on Alternating-Time Temporal Logic ATL and Coalition Logic CL (for example, [Pauly, 2001; Goranko, 2001; Pauly, 2002; Alur et al., 2002; Wooldridge et al., 2007]) has allowed the expression of many interesting properties of coalitions and strategies. However, there is no natural way of expressing resource requirements in these logics.

The motivation for this work is in verifying problems of the following form: can a set of agents C achieve a state of the world satisfying φ under the given resource bound b. Essentially, this is the successful coalition under resource bound problem from [Wooldridge and Dunne, 2006]. Unlike Wooldridge and Dunne [2006], we consider multi-shot games where the agents need to perform a sequence of actions to achieve the goal. As a motivating example, consider a system of distributed reasoning agents as described in [Alechina et al., 2008], whose actions involve inferring new clauses from their knowledge bases and communicating results to other agents. Clearly these activities require resources such as time (which can be identified with the number of inference steps), memory (the space required to store premises in reasoning, and any intermediate lemmata, which can be measured as the number of clauses in the agents memory at any one time) and communication bandwidth (which can be measured as the number of communicated clauses). Properties of interest for such systems include 'the set of reasoners A can derive the clause [p] under the resource bound 10 for time, 3 for memory and 2 for communication'. In general, we would like to be able to express any properties of systems where abilities of individual agents and coalitions of agents are constrained by available resources in a non-trivial way, and the properties relating to resource bounds are important.

∗This work was supported by the Engineering and Physical Sciences Research Council [grant number EP/E031226/1.]

In this paper, we propose a logic in which we can describe systems of agents specified in terms of the resources required to perform actions. First we introduce a simple formalism RBCL1 which describes single-step strategies and is based on Coalition Logic [Pauly, 2002] extended with resource bounds. We then motivate multi-step strategies and introduce a more complex logic RBCL which can express multi-step strategies (in a sense corresponding to the Extended Coalition Logic of [Pauly, 2001]). We give a sound and complete axiomatisation of RBCL.

2 Formalising Single Step Strategies

We assume a set of agents A = {1, . . . , n} and a set of resources R = {1, . . . , r}. Agents can perform actions from a set Σ = ∪i∈AΣi, where Σi is the set of actions agent i can perform. Each action a ∈ Σ has an associated cost Res(a), which is a vector of costs (assumed to be natural numbers) for each resource in R. A coalition C ⊆ A can execute a joint action aC, where aC is a tuple of actions (a1, . . . , ak) (we assume for simplicity unless otherwise stated that C = {1, . . . , k} for some k ≤ n). For the moment, let us stipulate that the cost of a joint action aC corresponds to the vector sum of costs of actions in aC (we will generalise the way to combine costs for different resources later). We compare vectors of resources using pointwise vector comparison ≤, e.g., for b = (b1, . . . , br) and d = (d1, . . . , dr), b ≤ d iff for each j ≤ r, bj ≤ dj.

The language of RBCL1 is defined relative to the sets A and R and a set of propositional variables Prop. A formula is defined as follows:

where p ∈ Prop, C ⊆ A, and b ∈ Nr . The intuitive meaning of [Cb ]φ for C ̸= ∅ is that coalition C can force the outcome ψ under resource bound b, or in other words C has a strategy costing at most b which enables them to achieve a φ-state no matter what the other agents ¯ C = A \ C do. For the empty coalition, [∅b ]φ means that if the grand coalition A executes any joint action which together costs at most b, then the system will end up in a φ state; that is, φ is unavoidable if A acts within resource bound b.

We define models of RBCL1 as transition systems, where in each state agents execute some actions in parallel which determines the next state. These are essentially the same as the models for coalition logic, with the addition of costs of actions. First we define action frames which underlie the models:

Definition 1. A resource-bounded action (RBA) frame F is a tuple (A, R, Σ = ∪i∈AΣi, S, T, o, Res) where:

A is a non-empty set of agents,

R is a non-empty set of resources,

Σ is the set of actions agents can perform,

S is a non-empty set of states,

• T : S ×A → ℘(Σi) assigns to each state the set of actions available to agent i in this state; this set is always nonempty as it contains an action noop with Res(noop) = ¯0 = (0, . . . , 0),
• o is the outcome function which takes a state s and a joint action aA and returns the state resulting from the execution of aA by the agents in s,

Res : Σ→Nr is the resource requirement function.

In the case of joint actions, we generalise the function T as follows: a joint action aC ∈ T(s,C) iff ai ∈ T(s, i) for all i ∈ C. By Res(aC) we denote the vector sum of Res(ai) for i ∈ C.

Definition 2. A single-step resource-bounded action model M is a pair (F, V ) where F is an RBA frame, and V : S → ℘(Prop) is an assignment function.

The truth definition for single-step RBA models is as follows:

• M, s |= p iff p ∈ V (s)
• M, s |= ¬φ iff M, s ̸|= φ
• M, s |= φ ∧ ψ iff M, s |= φ and M, s |= ψ
• M, s |= [C b ]φ for C ̸= ∅ iff there is aC ∈ T(s,C) with Res(aC) ≤ b such that for every joint action a ¯ C ∈ T(s, ¯ C) by the agents not in C, the outcome of the resulting tuple of actions executed in s satisfies φ: M, o(s, (aC, a ¯ C)) |= φ
• M, s |= [∅b ]φ iff the outcome of any joint action aA ∈ T(s,A) with Res(aA) ≤ b executed in s satisfies φ: M, o(s, aA) |= φ.

The notions of satisfiability and validity are standard. Let us call the set of all formulas valid in single-step RBA models RBCL1 (where 1 refers to considering only one-step strategies, as in Coalition Logic).

Theorem 1. RBCL1 is completely axiomatised by the following set of axiom schemas and inference rules:

A0 All propositional tautologies

• A1 [Cb ]⊤
• A2 ¬[Cb ]⊥
• A3 ¬[∅b ]ϕ→ [Ab ]¬ϕ
• A4 [Cb ](ϕ∧ψ) → [Cb ]ϕ

The notions of derivability and consistency are standard. Note that if we erase the resource superscript in the axiomatisation above, we get the complete axiomatisation of Coalition Logic as given in [Pauly, 2002], and a trivial formula resulting from A5. The rule of monotonicity (RM) is derivable, as in Coalition Logic, that is if ⊢ ϕ→ψ, then ⊢ [C b ]ϕ→ [Cb ]ψ.

We omit the completeness proof here as it is a special case of completeness proof of RBCL given below.

As an illustration, we state a property of the first example given in [Wooldridge and Dunne, 2006], that the coalition of agents 1 and 2 can achieve g1 within the resource bound (3, 2). This can be expressed in RBCL1 as [{1, 2}(3,2) ] g1.

3 FormalisingMulti-step Strategies and Arbitrary Resource Combinators

In what follows, we generalise the logic described above in two ways. First, we consider multi-step strategies, as in Extended Coalition Logic with the [C∗ ] operator [Pauly, 2001], or as in ATL. The reason for this is as follows. We are interested in the costs of strategies which involve multiple steps. For example, suppose a coalition C can enforce their goal φ in three steps: [Cb1 ][Cb2 ][Cb3 ]φ. We can deduce from this that the agents have a strategy to achieve φ which costs at most b1+b2+b3. However expressing the fact in this way is rather clumsy. Even worse, to say that 'C has some strategy which achieves φ in three steps which costs at most b', we have to use a disjunction over all possible vectors of natural numbers b1, b2, b3 which sum up to b: ∨b1+b2+b3=b[Cb1 ][Cb2 ][Cb3 ]φ. Hence we extend the set of actions, or strategies, with sequential compositions of actions.

The second direction of generalisation involves the way we calculate the resource requirements of complex actions. We argue that not all resource costs should be combined using simple addition. For example, if one of resources is time and the agents execute their actions concurrently, then if each individual action costs one unit of time, the parallel combination of those actions also costs one unit of time. If one of the resources is memory, one can argue that if action a1 requires n units of memory and action a2 requires m units of memory, then executing actions a1 and a2 sequentially requires max(n,m) units of memory. For generality, we introduce two cost combinators to express how amounts of resources are combined in parallel and sequentially. If two actions a1 and a2 are performed in parallel, then the cost of executing them is Res(a1) ⊕ Res(a2) and the cost of executing them sequentially is Res(a1) ⊗ Res(a2) (where ⊕ and ⊗ may be sum for some resources, and max or some other combinator for others).

In the rest of the paper, we assume that the set of resources R always includes time, that every action costs exactly one unit of time, and that the time cost is the last component of every cost vector. The cost of the noop action is redefined as (0, . . . , 0, 1). We denote by t(b) the time component of cost vector b. In particular, t(Res(a)) = 1 for any a ∈ Σ. In the language, only operators [Cb ] with t(b) ≥ 1 are allowed.

3.1 Strategies andMulti-step RBAModels

Given an RBA frame F = (A, R, Σ, S, T, o, Res), a strategy for an agent i ∈ A is a function fi : S+ → Σi from finite non-empty sequences of states to actions, such that fi(λs) = a ∈ T(s, i), where λs is a sequence of states ending in state s. Intuitively, fi says what action agent i should perform in state s given the previous history of the system. A strategy for a coalition C is a set FC = {f1, . . . , fk} of strategies for each agent.

For a sequence λ = s0s1 . . . ∈ Sω , we denote λ[i] = si and λ[i, j] = si . . . sj .

The set of possible computations generated by a strategy FC from a state s0, out(s0, FC), is

{λ | λ[0] = s0 ∧ ∀j > 0 : λ[j+1] ∈ o∗ (λ[j], (fi(λ[0, j]))i∈C)} where o∗ (s, aC) = {o(s, (aC, a ¯ C)) | a ¯ C ∈ T(s, ¯ C)}. Now we define the cost of a multi-step strategy. Let λ ∈ out(s0, FC). The cost of FC over a prefix λ[0,m] where m > 0 is defined inductively as follows:

Res(λ[0, 1], FC) = ⊕i∈CRes(fi(λ[0])) (where Res(fi(λ[0])) is the cost of the action by agent i in λ[0], and ⊕i∈C is the operator for combining the costs of actions executed in parallel by the agents in C)

Res(λ[0, m], FC) = Res(λ[0, m - 1], FC) ⊗ (⊕i∈CRes (fi(λ[0,m-1]))) for m > 1 (this is the cost of the previous m- 1 steps in the strategy combined sequentially with the cost of the mth step).

Definition 3. Amulti-step resource-bounded actionmodelM is a pair (F, V ) where F is an RBA frame, and V : S → ℘(Prop) is an assignment function, and the truth definition for the [Cb ] modality is

• M, s |= [C b ]φ for C ̸= ∅ iff there is a strategy FC such that for all λ ∈ out(s, FC), there exists m > 0 such that Res(λ[0, m], FC) ≤ b and M, λ[m] |= φ,
• M, s |= [∅b ]φ iff for all strategies FA, computations λ ∈ out(s, FA), and m > 0 such that Res(λ[0,m], FA) ≤ b, M, λ[m] |= φ.

The set of all formulas valid in multi-step RBA models will be denoted by RBCL.

3.2 Effectivity Structures

For proving completeness of RBCL, it is easier to work with an alternative semantics, given not in terms of multi-step RBA models, but in terms of effectivity structures. These are closely related to RBA models, and we will show that effectivity structures satisfying some natural properties give rise to an alternative semantics for RBCL.

Let ℘(A)B = {Cb | C ⊆ A, b ∈ Nr , t(b) ≥ 1}. Intuitively, this is the set of all possible coalitions with all possible resource allocations. An effectivity structure is a function E : S → (℘(A)B → ℘(℘(S))) which describes, for each state in S, which subsets of S a coalition C can force under resource bound b.

Given an RBA frame F, the effectivity structure corresponding to F is defined as follows:

• For C ̸= ∅, X ∈ E(s)(Cb ) iff there exists a strategy FC such that for all λ ∈ out(s, FC), there exists m > 0 such that Res(λ[0, m], FC) ≤ b and λ[m] ∈ X.
• X ∈ E(s)(∅b ) iff for all strategies FA, computations λ ∈ out(s, FA), and m > 0 such that Res(λ[0, m], FA) ≤ b, we have λ[m] ∈ X.

In other words, X ∈ E(s)(Cb ), where C is not the empty coalition, means that the coalition C has a strategy to bring about X within the bound b. X ∈ E(s)(∅b ) means that whatever the grand coalition does under the cost b, the system always goes to a state in X, i.e. it cannot avoid X.

3.3 Characterising Effectivity in RBA Frames

Every RBA frame gives rise to an effectivity structure, but the reverse does not hold. In this section, we characterise properties which an effectivity structure should satisfy to be an effectivity structure corresponding to an RBA frame. Following Pauly in [Pauly, 2002], we call such effectivity structures playable (RB-playable, where RB stands for resourcebounded).

Below we state some useful properties of RB-playable effectivity structures. These are very similar (apart from the resource bound) to the properties of playable effectivity structures listed in [Pauly, 2002] and are given the same names:

An effectivity structure E is outcome monotonic iff

An effectivity structure E is coalition monotonic iff

An effectivity structure E is A-maximal iff

An effectivity structure E is A-minimal iff X ∈ E(s)(Ab )∧Y /∈ E(s)(Ab ) ⇒X \Y ∈ E(s)(Ab ) (this property is not listed in [Pauly, 2002], but its analogue is derivable there)

An effectivity structure E is regular iff

An effectivity structure E is super-additive iff the following holds, for all t(b) = t(d) = 1, C ∩ D = ∅: - if C ̸= ∅ and D ̸= ∅, X1 ∈ E(s)(Cb ) and X2 ∈ E(s)(Dd ) ⇒ X1 ∩ X2 ∈ E(s)((C ∪ D)b⊕d ). - if C = ∅, X1 ∈ E(s)(∅d ) and X2 ∈ E(s)(Dd ) ⇒ X1 ∩ X2 ∈ E(s)(Dd ).

Note that super-additivity applies only to effectivity functions corresponding to single-step strategies (with the time component of the bound equal to 1). Since effectivity functions correspond to multi-step strategies, we need to extend superadditivity to more than single-step strategies, that is to the case when the time component is greater than 1:

An effectivity structure E is general super-additive iff it is super-additive and X1 ∈ E(s)(∅b ) and X2 ∈ E(s)(Cb ) ⇒ X1 ∩ X2 ∈ E(s)(Cb ).

We also need properties corresponding to sequential composition of strategies:

An effectivity structure E is super-transitive iff the following holds for all C ̸= ∅: {s′ ∈ S | X ∈ E(s′ )(Cb2 )} ∈ E(s)(Cb1 ) ⇒ X ∈ E(s)(Cb1⊗b2 ) (if a set of states where X is obtainable under b2 can be enforced under b1, then X can be enforced by the combined strategy under b1 ⊗ b2).

An effectivity structure E is transitive iff for any b with t(b) > 1 and C ̸= ∅: X ∈ E(s)(Cb ) ⇒ ∃b′ < b : X ∈ E(s)(Cb′ ) (X can be achieved under a tighter bound b′ ) or ∃b1 ⊗ b2 = b : {s′ ∈ S | X ∈ E(s′ )(Cb2 )} ∈ E(s)(Cb1 ) (X can be achieved by combining two strategies costing b1 and b2 such that b1 ⊗ b2 = b).

Finally, the following property is specific to resource bounds: An effectivity structure E is bound-monotonic iff

Bound-monotonicity is a very natural property: if a nonempty coalition can achieve something under the bound b, then it can achieve it with a more generous resource allowance. For C = ∅, this property means that if an outcome cannot be avoided when the grand coalition is restricted to strategies which cost at most b, then it cannot be avoided if A uses fewer resources (hence has fewer strategies available).

It is easy to prove that the properties above are true for any effectivity structure obtained from a RBA frame. Conversely, RB-playable effectivity structures defined below are effectivity structures of an RBA frame.

Definition 4. An effectivity structure E : S → (℘(A)B → ℘(℘(S))) is RB-playable iff, for every s ∈ S, E has the following properties:

1. For all Cb ∈ ℘(A)B , S ∈ E(s)(Cb )
2. For all Cb ∈ ℘(A)B , ∅ /∈ E(s)(Cb )
3. Outcome-monotonicity
4. A-maximality
5. Super-additivity
6. Super-transitivity
7. Transitivity
8. Bound-monotonicity

It can be shown that RB-playability implies the other properties listed above.

Lemma 1. Let E be a RB-playable effectivity structure, then E has the following properties:

1. Coalition monotonicity
2. A-minimality
3. Regularity
4. General super-additivity

The proof is omitted due to lack of space. First, general super-additivity is proved by induction on resource bounds using super-additivity, and the proof for other properties uses general super-additivity.

Theorem2. An effectivity structure is RB-playable iff it is the effectivity structure of some RBA frame.

Proof. It is easy to check that effectivity structures obtained from RBA frames satisfy all properties of RB-playability. For the other direction, given an RB-playable effectivity structure E, we will construct a RBA frame such that its effectivity structure is E.

Let E be RB-playable. The construction of the RBA frame is similar to that in Coalition Logic extended with costs for actions. First, we define the set of possible actions for each agent at each state s ∈ S with their associated costs Res. Then, the construction is completed by defining the outcome function o.

For i ∈ A and b such that t(b) = 1, we denote C b i = {Cd | i ∈ C ∧ t(d) = 1 ∧ d ≥ b} the set of all coalitions that i may participate in while contributing b amount of resources. Note that for all actions t(b) is always 1.

For s ∈ S, we define

Γ(s, i) is the set of option functions for an agent i at state s. Each option function in Γ(s, i) is a mapping gb i (s) which determines the outcome if agent i agrees to participate in a coalition. How an agent agrees to participate in a coalition will be specified later when we define the outcome function.

Let H = {h : ℘(S) → S|h(X) ∈ X} be the set of choice functions, that is if an agent has the power to decide the outcome, it will use some h function to do that. Then, we define the set of available actions for an agent i at a state s as follows:

Each action is a triple (gb (s), t, h) consisting of an option function gb , an index t (a natural number) and a choice function h. Informally, option functions will determine how the agents group together to form coalitions and then which outcome options they will choose. The index determines which agent has the power to decide the outcome based on its associated h function. For now, we assign that Res((gb (s), t, h)) = b.

Let Σi = ⋃s∈S T(s, i). We now define the outcome of a joint action σ ∈ ΣA at a state s. Assume that σ = {(gbi i (s), ti, hi)|i = 1, . . . , n} in which t(bi) = 1 for all i ∈ A. Let bC = ⊕i∈Cbi, g = (gbi i (s))i∈A. We denote P(f, C) the coarsest partition 〈C1, . . . , Cm〉 of C such that:

We define how coalitions are formed based on g as follows:

As A is finite, the above computation reaches some η such that Pη(g) = Pη+1(g). Let P(g) = Pη(g) which shows how agents are grouped into coalitions.

For technical convenience, let Eo (s)(Ab ) denote the collection of minimal sets in E(s)(Ab ). By A-minimality, it is easy to show that Eo (s)(Ab ) contains only singletons. In other words, by outcome-monotonicity, we have X ∈ E(s)(Ab ) if and only if X ⊇ Xo for some Xo ∈ Eo (s)(Ab ). By regularity, we have X ∈ E(s)(∅b ) if and only if X ⊇ ∪Eo (s)(Ab ).

Assume that P(g) = 〈C1, . . . ,Cm〉. For convenience, let g(Cl) = gbi i (Cl bCl ) for some i ∈ Cl where l ≤ m.

additivity and the fact that ∅ /∈ E(s)(AbA ) as E is RBplayable, it is straightforward to show that G(f) ̸= ∅.

Let t0 = (∑i∈A ti mod n) + 1. The outcome function is defined as follows: o(s, σ) = ht0 (G(g)). Let EF be the effectivity structure of the frame constructed above. We claim that E = EF .

Firstly, we show the left-to-right inclusion by induction on bounds. In the base case, assume X ∈ E(s)(Cb ) in which t(b) = 1. Choose the actions for agents in C as follows,

where gb1 (Dd ) = g0 i (Dd ) = X for all i = 2, . . . , k, D ⊇ C, d ≥ b. Notice that the choices of gb1 , g0 2 , . . ., g0 k must exist because of bound-monotonicity and coalition-monotonicity. Moreover, the choices of ti and hi, where i = 1, . . . , k, are arbitrary. Let σC = {(gb1 , t1, h1), (g0 2 , t2, h2), . . . , (g0 k , tk, hk)}.

Let σC be an arbitrary joint action for C. Let σ = (σC, σC ) and let g be the set of the option functions from σ. By the choice of σC, C must be a subset of a partition Cl in P(g). Then, we have

Hence, X ∈ EF (s)(Cb ).

For the induction step, let X ∈ E(s)(Cb ) in which t(b) > 1. If X ∈ E(s)(Cb′ ), by the induction hypothesis, we have X ∈ EF (s)(Cb′ ). Therefore, bound-monotonicity implies that X ∈ EF (s)(Cb ).

If X /∈ E(s)(Cb′ ) for any b′ < b, by transitivity there are b1 ⊗ b2 = b such that

By the induction hypothesis, we have

and

By outcome-monotonicity, we have

Hence, by super-transitivity X ∈ EF (s)(Cb ).

For the other direction, we consider two cases in which C = A and C ⊂ A.

Assume that X /∈ E(s)(Ab ). By A-maximality, we obtain X ∈ E(s)(∅b ). However, the previous proof implies that X ∈ EF (s)(∅b ). As EF is RB-playable, by regularity we have X ∈ EF (s)(Ab ).

For the case of C ⊂ A, the proof is done by induction on bounds. Assume that X /∈ E(s)(Cb ) in which t(b) = 1 and C ⊂ A, i.e. there is i0 ∈ A\C. Let σC = {(gbi i (s), ti, hi)|i ∈ C} be an joint action for C such that Res(σC) ≤ b. We choose a strategy for C σC = {(gbi i (s), ti, hi)|i ∈ C} such that:

• bi = 0 for all i > k
• gbi i (s)(Dd ) = S for all i ∈ C, D ⊇ C, d ≥ bi
• (∑i∈A ti mod n) +1 = i0
• hi for i ̸= i0 is arbitrary, we will select hi0 shortly

As before, let σ = (σC, σC ) and g the collection of option functions in σ. We use notation bD = ⊕i∈Dbi for any D ⊆ A.

By the choice of option functions in σC , it follows that C is the subset of some partition Cl of P(g). For other partitions, super-additivity shows that G(g) ∈ E(s)(Cl bCl ). By coalition-monotonicity and bound-monotonicity, we have that G(g) ∈ E(s)(Cb ). As X /∈ E(s)(Cb ), it follows that G(g) ̸⊆ X by outcome-monotonicity, i.e. there is some s0 ∈ G(g) \ X. Select hi0 such that hi0 (G(g)) = s0, then

Hence, X /∈ EF (s)(Cb ).

In the induction step, assume that X /∈ E(s)(Cb ) where t(b) > 1. Bound-monotonicity shows that for all b′ ≤ b, X /∈ E(s)(Cb′ ) and super-transitivity implies that for all b1⊗b2 = b,

By the induction hypothesis, we have that for all b′ < b, X /∈ EF (s)(Cb′ ) and for all b1 ⊗ b2 = b,

and {s′ | X ∈ E(s′ )(Cb2 )} = {s′ | X ∈ EF (s′ )(Cb2 ). Then, {s′ | X ∈ EF (s′ )(Cb2 )} /∈ EF (s)(Cb1 ). Therefore, transitivity implies that X /∈ EF (s)(Cb ).

4 Axiomatisation of RBCL

In this section we define models based on playable effectivity structures, and give a complete axiomatisation for the set of validities in those models.

Definition 5. A resource-bounded effectivity model M = (S,E, V ) is a triple consisting of a non-empty set of states, a RB-playable effectivity structure and a valuation function V : Prop → ℘(S). The truth definition for [Cb ] modalities is as follows:

Theorem 3. The sets of formulas valid in multi-step RBA models and in resource-bounded effectivity models are equal.

This follows from the correspondence between RBA frames and RB-playable effectivity structures, and the correspondence between the two truth definitions. Therefore the next result also provides an axiomatisation for RBCL.

Theorem 4. The following set of axiom schemas and inference rules provides a sound and complete axiomatisation of the set of validities over all resource-bounded effectivity models:

A0-A5, MP and Equivalence given above

• A6 [Cb ]ϕ∧[Dd ]ψ → [(C∪D)b⊕d ](ϕ∧ψ) where C∩D = ∅, t(b) = t(d) = 1 and b = d if either C or D is empty

Proof. The proof of soundness is straightforward. We concentrate on proving completeness. We prove completeness by constructing a canonical model. Let us denote by ⊢Λ derivability in the axiom system above. Let SΛ be the set of all Λ-maximally consistent sets. For any formula ϕ, we denote ˜ ϕ = {s ∈ SΛ | ϕ ∈ s}. Then, we define the canonical valuation function V Λ(p) = ˜ p.

We define the canonical effectivity structure EΛ by induction on b as follows:

• For all b such that t(b) = 1 and C ̸= A, X ∈ EΛ(s)(Cb ) iff ∃˜ ϕ ⊆ X : [C b ]ϕ ∈ s. X ∈ EΛ(s)(Ab ) iff X /∈ EΛ(s)(∅b ).
• For all b such that t(b) > 1 and C ̸= ∅, X ∈ EΛ(s)(Cb ) iff X ∈ EΛ(s)(Cb′ ) for some b′ < b or there are b1 ⊗ b2 = b such that {s′ | X ∈ EΛ(s′ )(Cb2 )} ∈ EΛ(s)(Cb1 ). X ∈ EΛ(s)(∅b ) iff X /∈ EΛ(s)(Ab ).

The following property (∗) is crucial for the proof:

We prove it by induction on the bounds. In the base case, assume that ˜ ϕ ∈ EΛ(s)(Cb ) for some t(b) = 1. For C ̸= A, ˜ ϕ ∈ EΛ(s)(Cb ) iff ∃ ˜ ψ ⊆ ˜ ϕ : [C b ]ψ ∈ s iff [Cb ]ϕ ∈ s (by ⊢Λ ψ → ϕ and RM). If C = A, we have ˜ ϕ ∈ EΛ(s)(Ab ) iff ˜ ¬ϕ /∈ EΛ(s)(∅b ) iff ¬[∅b ]¬ϕ ∈ s (as just proved) iff [Ab ]ϕ ∈ s (by axiom A3).

For the induction step, assume that ˜ ϕ ∈ EΛ(s)(Cb ) where t(b) > 1. For C ̸= ∅, there are two cases to consider. (1) ˜ ϕ ∈ EΛ(s)(Cb′ ) for some b′ < b. By the induction hypothesis, we have [Cb′ ]ϕ ∈ s. Then, axiom A5 implies that [Cb ]ϕ ∈ s. (2) There are b1 ⊗ b2 = b such that

By the induction hypothesis, we have ˜ [Cb2 ]ϕ ∈ EΛ(s)(Cb1 ), so [Cb1 ][Cb2 ]ϕ ∈ s. Therefore, by axiom A7 [Cb ]ϕ ∈ s. If C = ∅, we have ˜ ϕ ∈ EΛ(s)(∅b ) iff ˜ ¬ϕ /∈ EΛ(s)(Ab ) iff ¬[Ab ]¬ϕ ∈ s (as just proved) iff [∅b ]ϕ ∈ s (by axiom A3). The proof that EΛ is RB-playable is straightforward given

the property (∗), definition of EΛ and the axioms of Λ.

Since we have already shown (*), the truth lemma (M Λ, s |= ϕ iff ϕ ∈ s) is also straightforward.

As an illustration, we can state a property from [Alechina et al., 2008] that two reasoners can derive an empty clause within resource bounds 4 for memory, 1 for communication, and 5 for time: [{1, 2}(4,1,5) ] B2⊥.

5 Conclusions and FurtherWork

We have proposed a complete and sound logic RBCL where we can express costs of (multi-step) strategies and hence coalitional ability under resource bounds in multi-shot games. The logic is expressive enough to formalise decision problems of Coalitional Resource Games [Wooldridge and Dunne, 2006] and properties of resource-bounded communicating reasoners from [Alechina et al., 2008]. RBCL is related to both Coalition Logic and ATL. The [Cb ] operators (without resource bounds) in RBCL correspond to the [C∗ ] operator in Extended Coalition Logic which stands for a finite iteration of [C] modalities [Pauly, 2001], or to the 〈〈C〉〉F operator of ATL [Alur et al., 2002].

In future work, we plan to investigate automated verification of properties of RBCL using model-checking. The model-checking algorithm for ATL given in [Alur et al., 2002] can be modified to produce a model-checking algorithm for RBCL without increase in complexity. We anticipate that we may also be able to exploit resource bounds to optimise the model-checking algorithm or to use bounded model-checking for some properties.