Coalition Logic

Origin. Marc Pauly developed coalition logic (2000, 2002). Extends modal logic to reason about what groups of agents can achieve. Alternating-time Temporal Logic (ATL) by Alur, Henzinger, and Kupferman (1997, 2002) combines coalition power with temporal logic. Foundation for multi-agent system verification.

Models. Group strategic ability. What can a coalition of agents achieve together, regardless of what other agents do? "Agents A and B together can ensure φ" — even if agent C tries to prevent it. Models cooperation and competition among multiple agents with simultaneous actions.

Formalism.

Coalition Logic (CL):

Coalition modality: [C]φ — coalition C has a strategy to achieve φ in one step, regardless of what agents outside C do.

Agents: Agt = {1, 2, ..., n} Coalition: C ⊆ Agt

Semantics (effectivity functions): For each state s, effectivity function E(s): 2^Agt → 2^(2^States) E(s)(C) = sets of outcomes coalition C can force.

[C]φ true at s iff ⟦φ⟧ ∈ E(s)(C)

Properties:

• [∅]φ ↔ □φ (empty coalition = necessity)
• [Agt]φ ↔ ◇φ (all agents = possibility)
• Monotonicity: C ⊆ C' and [C]φ → [C']φ

Alternating-time Temporal Logic (ATL):

Adds temporal operators to coalition logic:

• ⟨⟨C⟩⟩○φ — C can ensure φ at next step
• ⟨⟨C⟩⟩□φ — C can ensure φ always
• ⟨⟨C⟩⟩◇φ — C can ensure φ eventually
• ⟨⟨C⟩⟩φUψ — C can ensure φ until ψ

ATL semantics (concurrent game structures):

• States, agents, actions, transition function
• At each state, each agent independently chooses an action
• Joint action determines next state
• ⟨⟨C⟩⟩φ: C has a strategy such that for all strategies of Agt\C, the outcome satisfies φ

ATL:* Adds strategy quantification and path formulas (like CTL* vs CTL).

Symbols.

Metatheory. Coalition logic satisfiability is PSPACE-complete (Pauly). ATL model checking is PTIME-complete, running in time linear in |model| × |formula| — not PSPACE in the formula, and it is exactly this linearity that makes ATL usable for verification; ATL satisfiability is EXPTIME-complete. ATL* is 2EXPTIME-complete for both model checking and satisfiability. Strategy Logic (more expressive) has non-elementarily decidable model checking, and its satisfiability is undecidable. Complete axiomatizations exist for CL and ATL. Coalition logic is not a fragment of multi-agent S5: [C] is a non-normal modality interpreted over monotone neighbourhood (effectivity) models and fails K, whereas S5 is a normal system — the two axiomatize ability and knowledge respectively.

Applies to. Multi-agent system verification. Social choice theory. Security (attacker coalitions). Game theory (coalition formation). Voting systems. Smart contracts. Protocol verification. Autonomous vehicles (multi-agent coordination).

Limitations. Everything usable rests on perfect information. Once agents see only part of the state and are given perfect recall, model checking becomes undecidable (Dima and Tiplea, 2011), and the memoryless variants that stay decidable secure this by denying agents memory rather than by solving the problem. The logic also conflates having a winning strategy with knowing one: ⟨⟨C⟩⟩φ quantifies over strategies without requiring them to be uniform on indistinguishable states, so it asserts ability the coalition may be unable to exercise. Strategies are not carried across nested modalities — each is evaluated afresh — so ⟨⟨C⟩⟩□⟨⟨C⟩⟩◇φ does not say that one commitment achieves the goal. Coalitions are given, not formed, and agents have no preferences, so the framework expresses power but no solution concept and no equilibrium.

© 2026 Lingenic LLC