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.

Symbol	Unicode	Name	Meaning
[C]	—	Coalition modality	C can achieve (CL)
⟨⟨C⟩⟩	—	Coalition path	C can ensure (ATL)
○	U+25CB	Next	Next state
□	U+25A1	Always	All future states
◇	U+25C7	Eventually	Some future state
U	—	Until	Until
Agt	—	Agents	All agents
∅	U+2205	Empty coalition	No agents
C	—	Coalition	Subset of agents

Metatheory. Coalition logic is PSPACE-complete. ATL model checking is polynomial in model size, PSPACE in formula size. ATL* is 2EXPTIME-complete. Strategy Logic (more expressive) is non-elementarily decidable. Complete axiomatizations exist for CL and ATL. Coalition logic = multi-agent S5 fragment.

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. Perfect information assumed; agents know the full state. Strategies are memoryless in basic ATL; memory requires extensions. Coalition formation process not modeled (assumes coalitions given). Computational cost grows with agent number. Imperfect information variants (ATLiR) are harder. Real multi-agent systems have continuous actions, noise, uncertainty.