Coalitions in Action Logic

1 Introduction

In the last decade, there has been increasing interest in logics suited for reasoning about groups of agents [1; 9; 4; 11; 10] and some systems emerged as paradigmatic in this area. Among these, Pauly's Coalition Logic [8; 9] seems to identify the core properties of coalitions and it is practically taken as a parametric system to verifying the adequacy of other logics in this area.

Generally, these modal logics for coalitions address the relationship between models and relative expressivity of the systems without tackling the relationship between coalition power and each agent's actions. They essentially capture implicit coalition power as in "coalition C can enforce proposition ϕ", which here we contrast with logics of explicit coalition power, "coalition C, doing such and such, can enforce proposition ϕ". The relationship between these two types of systems must be studied if we want to be able to use the general view provided by coalition logics in frameworks where actions and their consequences can be evaluated (cf. [10]). The study of such a relationship is the goal of this work.

The first issue is the choice of the target language that can relate coalition power to agents' actions. One way to represent coalition power is to introduce a unary modality with two indices, say [C, a], where C is a coalition and a is an action; informally, given a proposition p, formula [C, a]p stands for "coalition C can enforce p by performing action a". If a coalition C is capable of enforcing p, we need a coalition action to express this fact in the language. If a model has n A way out is to refer to actions without actually naming them. This seems to match the general idea of Coalition Logic since, informally, what it captures is not "action such and such performed by C enforces p" but "C has a way to enforce p", i.e., "there exists a coalition action for C to enforce p". This latter approach guarantees a concise language by introducing quantifiers. We can implement it in two ways: on the one hand using variables for coalition actions and, on the other hand, using variables for agent actions. At a closer analysis, the first option gives us [C, ∃x] which does not differ in expressive power from Pauly's coalition modality [C].

The other option is what we study in this paper and requires a logic with new features. Such a logic has already been studied with other motivations in [3]. Here we isolate a fragment of that system and show how to translate coalition logic in it.

Overview: sections 2 and 3 present the coalition logic (CL) and the action logic (AL). Section 4 discusses the assumptions of the translation and defines the coalition action logic CAL. Sections 5 and 6 give the model correspondence. Section 7 discusses the approach and the notion of ability.

2 The Coalition Logic CL

The coalition logic CL [9] is a modal system for reasoning about groups of agents. The logic is developed to formally prove what a coalition of agents can bring about in a multiagent system. The semantics associates an (extensive) game of perfect information to each state in the system. The central notion is effectiveness: a coalition of agents is effective for a set of states in a game if the coalition can guarantee that the system will necessarily move to one state in the set [7].

The language of CL is a type of propositional multi-modal logic. It is built out of a countable set of proposition identifiers PropId, with ⊥ ∈ PropId, and contains 2|N| modal operators for some fixed finite set N. The modality markers are the subsets of N: [C] is a modality in CLif and only if C ⊆ N. Formulas in CL are defined inductively:

1. all elements of PropId are formulas (atomic formulas)
2. ϕ ∨ ψ and ¬ϕ are formulas if ϕ and ψ are formulas
3. [C]ϕ is a formula if C ⊆ N and ϕ is a formula

The intuition behind the formalism is that the modal operator [C] expresses the power of the group C of agents. The formula [C]ϕ states that the agents in C, acting as a coalition, can enforce ϕ no matter what the remaining agents do.

The semantics is based on game frames [9] that here we dub standard coalition frames. Note that standard coalition frames are not Kripke frames because modalities in CLdo not satisfy the normality condition, i.e, they do not distribute over implication.

Definition 2.1 (Coalition Frame)

A Coalition Frame for a set N is a pair FN = 〈W, R〉 where W is a non-empty set (the set of states) and R is a subset of W ×P(N) ×P(W). Furthermore, for all s ∈ W, C ⊆ N, and X, X′ ⊆ W, R satisfies the following:

III) If (s, ∅,X) ̸∈ R, then (s,N,W \X) ∈ R

Pauly [9] introduces R as a function R : W → (P(N) → P(P(W))). The two definitions are equivalent.

Proposition 2.1 (Coalition monotonicity) For all s ∈ W and C ⊆ C′ ⊆ N, (s, C, X) ∈ R → (s, C′ , X) ∈ R.

Definition 2.2 (Coalition Structure)

A Coalition Structure for a set N is a triple MF = 〈W, R, llbracket·rrbracket〉 where:

• 〈W,R〉 is a coalition frame FN;
• llbracket·rrbracket is a valuation function PropId ↦→P(W) s.t. llbracket⊥rrbracket = ∅.

Since N is fixed in advance, we drop it in FN. Also, we write R(C) for the set of pairs (s, V ) such that (s, C, V ) ∈ R and R(s)(C) for the set of sets V such that (s, C, V ) ∈ R.

Fix a coalition structure MF and a state s. We write MF, s |= ϕ to mean that the CL-formula ϕ is true (equivalently, satisfied) at state s of structureMF.

1. MF, s |= p if s ∈ llbracketprrbracket (for p atomic)
2. MF , s |= ¬ϕ if MF , s ̸|= ϕ
3. MF , s |= ϕ ∨ ψ if MF , s |= ϕ or MF , s |= ψ

We write MF |= ϕ to mean that formula ϕ is valid in MF, that is, it is true at each state ofMF. A coalition model for a set of formulas Σ in CL is a structureMF such that all formulas ϕ ∈ Σ are valid in MF . We write F |= ϕ to mean that ϕ is valid in each model based on frame F.

The interpretation of modal operators in CL follows the approach called minimal models [5], cf. clause 4). From condition I) on relation R, a structure for CL is serial with respect to all the modalities.

Axioms for Coalition Logic:

CL is determined by the class of coalition structures [9].

3 The Action Logic AL

We consider the multi-agent modal logic given in [3]. This language has the characteristics of merging modalities and quantifiers to model true concurrency, and was shown to be complete and decidable with respect to Kripke semantics. For our task, we will apply the fragment of this system selected below and that we dub AL.

Fix a set PropId of proposition identifiers, with ⊥ ∈ PropId, and a disjoint set of variables, Var. We will use pi for proposition identifiers and xi for variables.

Definition 3.1 (Modality Marker for AL)

A modality marker for AL is a k-column of quantified variables

To maintain a direct connection 1 with [3], no variable can occur more than once in a modality marker.

The set of formulas for AL is the smallest set satisfying the following clauses:

1. all elements of PropId are formulas (atomic formulas)

b. ϕ ∨ ψ and ¬ϕ are formulas if ϕ and ψ are formulas

1. [M]ϕ is a formula if M is a modality marker and ϕ is a formula

(From this, all AL formulas turn out to be closed.)

There is an obvious bijection between the set of modality markers and the set of modal operators in the language. We will use the two notions indifferently.

Definition 3.2 (k-Action) Given a set Act of actions, a k-

α1 α2

action is any column of k elements .. αk with αi ∈ Act. 2

Definition 3.3 (Multi-agent Kripke Frame for AL)

• A Multi-agent Kripke Frame for AL is a triple K = 〈W, Act , R〉 where:
• W is a non-empty set (the set of states),
• Act is a non-empty set (the set of actions), and
• R is an (accessibility) relation mapping k-actions A, over Act, to binary relations on W: R(A) ⊆ W ×W.

Definition 3.4 (Multi-agent Kripke Structure for AL)

• A Multi-agent Kripke Structure for AL is a 4-tuple MK = 〈W, Act , R, llbracket·rrbracket〉 where:
• 〈W,Act,R〉 is a multi-agent Kripke frame K;
• llbracket·rrbracket is a valuation function PropId ↦→P(W) s.t. llbracket⊥rrbracket = ∅.

In the remaining of the paper, we use the terms Kripke frames (structures, respectively) to refer to multi-agent Kripke frames (structures).

Definition 3.5 (Instances) Fix a k-action A and a modality marker M. A(i) (M(i), resp.) is the i-th entry of A (M). For each j, we say that A(j) instantiates the j-th variable of M.

1 This connection is a central motivation for this work (section 7) and justifies our use of columns as modality markers.

2 In [3] these are called "basic k-actions."

Fix a Kripke structure MK and a state s. Relation |= is defined recursively for MK as follows:

1. MK, s |= p if s ∈ llbracketprrbracket (for p atomic)
2. MK, s |= ¬ϕ if MK, s ̸|= ϕ
3. MK, s |= ϕ∨ψ if MK, s |= ϕ orMK, s |= ψ
4. Let x1, . . . , xr (r ≥ 0) be all the existentially quantified variables in M and let xj occur at M(ij), MK, s |= [M]ϕ if ∃α1, . . . , αr ∈ Act (αm, αn not necessarily distinct) such that for all k-action A with A(ij) = αj (i.e., αj instantiates xj inM) for all j ≤ r, if (s, s′ ) ∈ R(A) thenMK, s′ |= ϕ.

We writeMK |= ϕ to mean that formula ϕ is valid inMK, that is, it is true at each state ofMK. AKripke model for a set of formulas Σ in AL is a structureMK such that all formulas ϕ ∈ Σ are valid in MK. We write K |= ϕ to mean that ϕ is valid in each model based on frame K.

Let k be the number of agents in the multi-agent system one wants to model. Fix an arbitrary order of the agents and let A1 be the first agent, A2 the second agent, . . . , Ak the k-th agent. Technically, a formula [M]p with existential entries i1, i2, . . ., is true in a state s when there exist values for the existentially quantified variables such that no matter the values selected for the universally quantified variables, the corresponding k-action brings (through R) only to states verifying p. From the point of view of a multi-agent system, a formula [M]p is true if the agents Ai1 , Ai2 , . . . (those whose positions correspond to existential entries of M) can perform a set of actions that force p to be verified no matter the actions executed by the remaining agents. (The general perspective behind AL is presented in [2].)

4 The Coalition Action Logic CAL

In this section, we analyze the relationship between CL and AL. A byproduct of this comparison is the clarification of a common misunderstanding on the notion of coalition in CL .

At the core of Coalition Logic there is the notion of effectiveness which is taken from the theory of social choice [7]. This notion captures the case of a group of agents that can force the system to evolve to states where some given property holds, no matter what the other agents do. The actions of these agents are thus effective in achieving the goal. Adopting such an interpretation, one assumes that the realization of the property is a common goal for the agent in the coalition and that they are capable of and intend to coordinate their actions. As a slogan, one can say that Coalition Logic studies the existence of a joint strategy for a common goal (the strategy itself is unspecified and possibly unknown). This approach is part and parcel of the view proposed by Coalition Logic, i.e., that of a system as a whole where the references to agents are more a way of speaking at the informal level than an effective (no pun intended) necessity.

Recall the informal reading of [C] in CL: formula [C] p stands for "the group C of agents has the power to enforce a state where p holds." Assume that there are k (k ≥ 1) agents in the multi-agent system and that an ordering of the agents has been fixed. Let agents A1, A2, . . . , Ar form group C. From the semantics of AL, it is natural to associate [C] p with the following formula of AL (let p be a formula in both CL and AL):

Thus, we can identify this set C with the set of indices {1, . . . , r}. The modality in (1) is not normal, due to the existential quantifiers occurring in it, although all its instances are. This fact is at the core of the connection between CL and AL. However, things do not work quite right. Exploiting the previous correspondence, we connect modality [∅] (for the empty coalition) to

Note that [∅] can bring about non-trivial consequences. 3 Since in AL only agents have this power and since [∅] corresponds to a coalition with no member, the correspondence given by (2) falls short to model the CL modality. 4 There are two possible ways out: to enrich the formalization of CL by constraining further modality [∅] or to accept (and motivate) the above peculiarity of CL by capturing it in the translation. The two choices have different consequences. Here we follow the second option. (For the first, proceed according the method given below using operators (1) and (2).)

The correspondence we formalize is between a CL system with k agents and an AL system with k + 1 agents as follows

In this way, the new agent (associated to x0 in row 0) is always in the coalition group. If the coalition C is empty, then the agent at row 0 is the only member of the corresponding coalition in CAL. What is the role of the new agent? Formally, it makes the translation possible since it allows to discriminate applications of the [∅] operator. Informally, it justifies the fact that an "empty coalition" can bring non-trivial consequences. The 0-th agent plays the role of the environment of the system (or nature for a more suggestive reading) whose power corresponds to that of the empty coalition in CL . In short, we can say that the axiomatization of CL makes sure that a coalition can force some state provided the environment plays on its side.

Since the agents in a coalition, say A0, A1, . . . , Ar, act according to a joint strategy, the choices at the existential entries (here entries at columns 0 to r) have to be made allowing full coordination. This means that the existentially quantified variables x0, x1, . . . , xr are instantiated at the same time, i.e., sequentially as they were forming an unbroken prefix list bounded by a unique existential quantifier. Furthermore, the joint strategy of the agents does not depend on the actions performed by the remaining agents since the agents are acting simultaneously. That is, the instantiation of variables x0, x1, . . . , xr does not depend on the values chosen for variables xr+1, . . . , xk. This argument illustrates that the semantics inherited from CL through the translation given above, corresponds to the semantics of AL. Needless to say that CL and AL are equivalent on the (common) propositional fragment of their languages.

3 This observation does not apply when modality [∅] is forced to be universal, i.e., if for all s, (s, ∅,X) ∈ R implies X = W.

4 An orthogonal issue is the normality of modality (2) which, generally speaking, might not be a desired property for [∅], although it is forced by the CL system of section 2.

Fix k + 1 variables: x0, x1, . . . , xk. We call CAL the language AL (for k + 1 agents) restricted to operators [M] such that M(0) = ∃x0 and M(i) = Qixi with Qi ∈ {∀, ∃}. (Note that the first entry in a modality for CAL has index 0. In this way, we preserve the correspondence of the agents A1, . . . , Ak in CL and in CAL.) The other characteristics of CAL are easily inherited from section 3.

Assume CL and CAL have the same proposition identifiers PropId (with ⊥ ∈ PropId). According to (3) we define a one-to-one function τ from CL to CAL as follows

• 1τ) if p ∈ PropId, then τ(p) = p;

We sometimes write [Cτ ] for the τ-image of operator [C] of CL , i.e., τ([C]) = [Cτ ].

5 FromCL-Frames to CAL-Frames

The next step is to show how this translation behaves with respect to the truth-values of formulas. We take care of this aspect providing a procedure that, given a frame for CL , determines a frame for CAL with the following properties: (a) the frames have the same states and (b) for all CL-formulas ϕ, ϕ is true at a state s in the CL -frame (for some interpretation for the propositional variables) if and only if τ(ϕ) is true at the corresponding state s in the CAL-frame (for the same interpretation.)

Fix a set N = {1, . . . , k} and the language of coalition logic CL . The language CAL has the same propositional identifiers of CL and variables x0, x1, . . . , xk only.

Fix a CL -frame for N, say, F = 〈W, RF 〉. The algorithm we are going to describe consists of two parts: subalgorithm A defines the set Act and subalgorithm B the relation RK. These are the elements needed to isolate a Kripke frame K = 〈W,Act,RK〉 for CAL.

[Subalgorithm A] With each state s ∈ W associate a set 6 Ds (Ds ∩Dt = ∅ for all states s, t). For any state s and set Ds , proceed as follows.

Basic case:

5 To fully determine τ, fix k + 1 variables, say x0, x1, . . . , xk, and use these at positions 0, 1, . . . , k (resp.ly) in all modalities.

6 The size is bounded above by 2k × |W|.

Let Ds 0 be the set of constants αV selected at this step.

General case:

Let Dsm be Dsm-1 plus the set of constants αV i1,...,im selected at this step.

Put ⋃s∈W Dsk = Act . This will be the set of actions in the frame of CAL.

We now define relation RK ⊆ {k + 1-actions} × W × W via subalgorithm B. Let P be the set of pairs <α, (s, C, V )> isolated at steps (A.0), . . . , (A.k). As usual, we write s′ ∈ RK(s)(A) or (s, s′ ) ∈ RK(A) to mean (A, s, s′ ) ∈ RK.

[Subalgorithm B] For α ∈ Act and I = {i1, . . . , im}, let Mα,I be any k + 1-action A such that A(j) = α for j ∈ {0}∪I. Let Mα,I - be any k+1-action A such that A(0) = α and A(j) ̸= α for some j ∈ I. We start with RK = ∅.

Basic case:

General case:

(B.m) given pair < α, (s, I, V ) > ∈ P, for all Mα,I,Mα,I -

• put (s, s′ ) ∈ RK(Mα,I) for all s′ ∈ V ,
• put (t, u) ∈ RK(Mα,I ) for all t, u ∈ W with t ̸= s,
• put (t, u) ∈ RK(Mα,I -) for all t, u ∈ W

From section 2, for all s in W and C ⊆ {1, . . . , k}, there exists V ⊆ W, V ̸= ∅, such that (s,C, V ) ∈ RF . Since all elements of Act have been introduced at some step (A.0), . . . , (A.k) for some s ∈ W and because of the second condition in (B.m), it follows that for any state s and any k + 1-action A, there exists s′ such that (s, s′ ) ∈ RK(A). In modal logic lingo, this property tell us that any multi-agent Kripke frame resulting from this algorithm is serial.

Having completed the definition of RK, we can finally put the pieces together. The frame for CAL is given by KF = 〈W,Act,RK〉 which is a Kripke frame for the multi-agent logic. Our next task is to verify the properties of frames F and KF. For this task, we will need the following lemma which follows by induction from the previous algorithm (note the special role of action α0).

Clearly, the two frames F = 〈W,RF 〉 and KF = 〈W,Act,RK〉 have same support. Since the languages have the same propositional variables, without loss of generality we can use the same valuation function llbracket·rrbracket for both systems.

Fix a formula ϕ of CL . If ϕ does not contain modal operators, then ϕ = τ(ϕ) and the two relations RF ,RK are inconsequential for the truth-value of ϕ.

To show that 〈F, llbracket·rrbracket〉, s |= ϕ if and only if 〈KF, llbracket·rrbracket〉, s |= τ(ϕ) for each sentence ϕ of CL , we proceed by induction. Assume 〈F, llbracket·rrbracket〉, s |= ϕ iff 〈KF , llbracket·rrbracket〉, s |= τ (ϕ) with ϕ wellformed formula in CL . We show that for all operators [C] in CL: 〈F, llbracket·rrbracket〉, s |= [C]ϕ ⇔ 〈KF, llbracket·rrbracket〉, s |= [Cτ ]τ(ϕ), where the relations |= refer to CL and to CAL, respectively.

Without loss of generality, let [C] = [{1, . . . , r}]. Let us write Z = ( z0 z1 .. zk ) with zi new variables ranging over Act. Then, 〈KF, llbracket·rrbracket〉, s |= [Cτ ]τ(ϕ) ⇔ ∃z0 . . . zr ∀zr+1 . . . zk if (s, s′ ) ∈ RK(Z) then 〈KF, llbracket·rrbracket〉, s′ |= τ(ϕ). By inductive hypothesis, the latter holds ⇔ ∃z0 . . . zr ∀zr+1 . . . , zk if (s, s′ ) ∈ RK(Z) then 〈F, llbracket·rrbracket〉, s′ |= ϕ. Now, put V = {t | 〈F, llbracket·rrbracket〉, t |= ϕ}. To prove our claim, it suffices to show: V ∈ RF (s)({1, . . . , r}) iff

Definition 5.1 Given an operator [M], we write Us(α, r), where α ∈ Act and r≥0, for the set of states reachable from s through k + 1-actions A for which A(j) = α (0 ≤ j ≤ r)

Note that, from the definition of Act and subalgorithm B, Us(α, r) is non-empty for all α ∈ Act. By Lemma 5.1, it suffices that: V ∈ RF (s)({1, . . . , r}) ⇔ ∃α . Us(α, r) ⊆ V .

First, consider case V = ∅. From Def 2.1, condition I), ∅ ̸∈ RF (s)(C). On the other hand, we already observed that Us(α, r) ̸= ∅ for all r ≤ k.

Consider now V ̸= ∅.

From left to right. By recursion on the size of C we prove a stronger claim, that is, there exists α such that Us(α, r) = V . Case C = ∅. Let V ∈ RF (s)(∅). By construction, step (A.0), there exists α ∈ Act such that for all βi ∈ Act, V ⊆

to show V ⊇ Us(α, r). If t ∈ Us(α, r), then (s, t) has been included in the definition of RK ( α β1 .. βk ) for some β1, . . . , βk.

From steps (A.0) and (B.0), the minimality of RK and the use of a different action at row 0 at each step (A.m), we have t ∈ V . Thus, Us(α, r) = V .

Assume the statement holds for |C| < r ≤ k. We show it holds for |C| = r. Without loss of generality, let C = {1, . . . , r} and fix V ∈ RF (s)({1, . . . , r}). By construction, step (A.r), there exists action α such that V ⊆ Us(α, r). Let t ∈ Us(α, r). Since at each step (A.m), a different action is used, (s, t) must have been included while considering pair < α, (s, {1, . . . , r}, V ) >. Thus, t ∈ Us(α, r) implies t ∈ V , i.e., Us(α, r) = V .

From right to left. Without loss of generality, we consider sets {1, . . . , r} with 0 ≤ r ≤ k. Let α be such that Us(α, r) ⊆ V , we show V ∈ RF (s)({1, . . . , r}). Here the recursion proceeds backward on the size of C from C = {1, . . . , k} to C = ∅. Since we apply a backword recursion, at step r (0 ≤ r < k) it suffices to consider sets V such that Us(α, k - r) ⊆ V and Us(α, k - (r + 1)) ̸⊆ V .

Case C = {1, . . . , k}. Consider set V with Us(α, k) ⊆ V and Us(α, k - 1) ̸⊆ V . From the construction and the Lemma 5.1, α must have been introduced at step (A.k). Let V ′ be the set for which α has been introduced. By construction, (s, {1, . . . , k}, V ′ ) ∈ RF so that V ′ ⊆ Us(α, k). Thus, V ′ ⊆ V and, by property IV ) of RF (see definition 2.1), (s, {1, . . . , k}, V ) ∈ RF , i.e., V ∈ RF (s)({1, . . . , k}).

Assume now that the statement holds for C = {1, . . . , r + 1}. We show it holds for C = {1, . . . , r}.

Let Us(α, r) ⊆ V and Us(α, r - 1) ̸⊆ V . This condition implies α has been introduced at step (A.r) for some set V ′ . V ′ ⊆ Us(α, r) follows by construction, thus V ′ ⊆ V . Finally, V ∈ RF (s)({1, . . . , r}) is obtained by condition IV ) of RF (see Definition 2.1) as before.

Case C = ∅ is analogous.

Theorem 5.1 For any frame F, valuation function llbracket·rrbracket, state s, and CL -formula ϕ

For any frame F and CL -formula ϕ

6 FromCAL-frames to CL-frames

Let K be a frame for CAL satisfying (1τ )-(5τ ), i.e., the τimages of axioms (1)-(5). 7 A frame FK for CL is obtained by defining RF to be minimal such that if V = {s′ | (s, s′ ) ∈ RK(A)} and A = ( α0 α1 .. αk ), then (s, C, V ) ∈ RF where C = {i | 1 ≤ i ≤ k and A(i) = α0}. It is easy to verify that

Theorem 6.1 For any frame K satisfying (1τ )-(5τ ), valuation function llbracket·rrbracket, state s, and CL -formula ϕ

For any frame K and CL -formula ϕ

7 Discussion and Conclusions

We presented a translation between two logics of agency that have been developed independently: a logic of coalition power (CL ), where actions are only implicit, and (a fragment of) a logic for groups of agents with individual actions (AL). AL models in detail the concurrent and interactive activity of the agents while CLcoarsens the description by focusing on groups and by disregarding individual actions. Our work provided a way to switch from one representation to the other and can also be used to refine proposals like [10]. Technically, we first isolated a fragment of AL, called CAL, which is isomorphic to the language of CL (sect. 4). Second, we showed that the Kripke semantics of CAL and the minimal semantics of CL agree (sect. 5). Finally, we showed that for each model for CL there is a corresponding CAL-model and vice versa (sect. 5 and 6). We observe that CAL is a fragment of a language determined by the class of multi-agent Kripke frames [3] while CL is determined by its class of minimal frames. Although CAL itself is not determined by the class of K frames satisfying (1τ )-(5τ ) (note that the last axiom fails due to the existential in row 0), it provides the needed connection between these two determined systems.

7 Note that (2τ ) and (4τ ) are always satisfied in CAL-frames. Axiom (1τ ) gives seriality on all the modalities. The remaining axioms are specific to the interaction of coalitions.

An Example

Consider a CL system with one agent and two states, say t and n. At state t, the actual state, the agent is thirsty. At state n the agent is not. Assume that the empty coalition [∅] (corresponding to the environment in CAL) has the power of making impossible to reach n, e.g., blocking tap water. Thus in CL , (t, ∅, {t}) ∈ R and, by II) in Def. 2.1, (t, ∅, {t, n}) ∈ R. The other coalition C = [1] (that is, the agent plus the environment) has the power to reach n, e.g., making tap water available (by the environment) and drinking (by the agent). Let us assume this coalition has no other power. Then, (t, {1}, {n}) ∈ R and, by II) again, (t, {1}, {t, n}) ∈ R. By subalgorithm A, we get four actions at this state, say Actt = {α, β, γ, δ}, for the triples above (in the given order). From subalgorithm B, (1) {t} = R( αx )(t) for any x ∈ Actt; (2) {t, n} = R( βx )(t) for any x ∈ Actt; (3) {n} = R( γγ )(t) and {t, n} = R( γx )(t) if x ̸= γ; (4) {t, n} = R( δx )(t) for any x∈ Actt. Two observations are in order. First, the elements of Actt obtained from the algorithm correspond to action-plans: γ at row 0 has different meaning than γ at row 1. That is, these are not action-types, their meaning depends on the agent performing them. A renaming is needed to move from action-plans to action-types. Second, different actions, like βγ and δδ , may bring to the same states. However, they capture different situations: with the first the environment prevents from reaching n, with the latter they both act so that the output is not determined. Only in the second case the result is due to a cooperation.

Ability

One important motivation for logics of groups is to study the notion of ability. Ability may vary in strength: α-ability (effectiveness) tell us that some agents can force ϕ no matter what the other agents do; β-ability that some agents can force ϕ provided they know what the other agents are going to do; and contingent ability that some agents can force ϕ provided the other agents do nothing (see [11] and references therein). CL focuses on effectiveness only and the interpretation of CAL we have adopted corresponds to the same notion: αability (also known as ∃∀-capability) is captured by the semantic clause 4. (section 3), which is of form: "there exist a list of actions ⃗α such that for all lists of actions ⃗β, . . .". Contingent ability is obtained by adding a "null action" (ε) in CAL and substituting ε for the universal quantified variables in the modal operators. Finally, β-ability (∀∃-capability) cannot be captured in the semantics of CAL (cf. [2]).

The Translation

Translations fromminimal to normal logics exist already [6]. We have not applied existing methods since they do not preserve important aspects of the structures. Indeed, the correspondence between the worlds in the models of CLand those in the models of CAL as well as the connections between these worlds are crucial to make explicit the relationship between agents, individual actions, and coalition power. A drawback is seen in the dimension of the target model since the size of Act is comparable to that of RF . Of course, one can make less distinctions. For instance at step (A.m) one may require that a new action αV i1,...,im is added only if (s, I, V ) ̸∈ RF for all I ⊂ {i1, . . . , im}. However, this new clause does not do justice of the notion of coalition since [C]p and [C′ ]p, with C ⊂ C′ , are now associated to the same action. If the two coalitions enforce p using the same individual actions, the extra agents of the larger coalition C′ are factually irrelevant. Instead, the algorithm of section 5 links the two coalitions to two different actions. This is important to relate CAL (and in turn CL ) to logics that can model strategies and plans since, generally speaking, bigger coalitions may have more alternative strategies and plans available.

Acknowledgments

Work partially funded by the PAT (Trento, IT) with projects "Mostro" and "Logical Instruments for Ontology Analysis". The author thanks the reviewers for their helpful comments.