Alternating-time Temporal Logic

Origin. Alur, Henzinger, Kupferman (2002). Strategic reasoning in multi-agent systems. Coalition modalities: ⟨⟨A⟩⟩φ. Agents can enforce properties. Foundation for game-theoretic verification.

Models. Concurrent game structures. Agents choose actions simultaneously. Coalitions: groups of agents. Strategy: function from histories to actions.

Formalism.

Coalition modality: ⟨⟨A⟩⟩φ: coalition A has strategy to ensure φ A ⊆ Agents (subset of agents)

Path quantifiers with strategies: ⟨⟨A⟩⟩○φ: A can ensure φ next step ⟨⟨A⟩⟩□φ: A can ensure φ always ⟨⟨A⟩⟩◇φ: A can ensure φ eventually ⟨⟨A⟩⟩φUψ: A can ensure φ until ψ

Semantics: q ⊨ ⟨⟨A⟩⟩φ iff ∃ strategy σ_A for coalition A such that ∀ counter-strategies of opponents: resulting plays satisfy φ

Special cases: ⟨⟨∅⟩⟩φ ≡ Aφ (for all paths) ⟨⟨Agents⟩⟩φ ≡ Eφ (exists a path)

Example: ⟨⟨{robot}⟩⟩◇goal "Robot has strategy to eventually reach goal"

⟨⟨{env}⟩⟩□¬safe → ¬⟨⟨{sys}⟩⟩□safe "If environment can prevent safety, system cannot guarantee it"

ATL:* Drops ATL's restriction that ⟨⟨A⟩⟩ be immediately followed by a single temporal operator: any LTL path formula may appear in its scope, so ⟨⟨A⟩⟩(□◇p → ◇q) is well-formed in ATL* but not ATL. More expressive, higher complexity.

Symbols.

Symbol	Unicode	Name	Meaning
⟨⟨A⟩⟩	—	Coalition modality	A has a strategy to enforce the argument
⟨ ⟩	U+27E8, U+27E9	Mathematical angle brackets	Doubled to form the coalition modality
○	U+25CB	White circle	Next: one step along the play
□	U+25A1	White square / Box	Always: invariant along the play
◇	U+25C7	White diamond	Eventually: reachability along the play
U	—	Until	φ holds until ψ does
A, E	—	Path quantifiers	For all plays; for some play, as in CTL
∅	U+2205	Empty set	The empty coalition, for which ⟨⟨∅⟩⟩ is A
⊆	U+2286	Subset of or equal to	A is a subset of the agents
∃	U+2203	There exists	Existential over strategies for A
∀	U+2200	For all	Universal over opponents' counter-strategies
σ	U+03C3	Greek small sigma	A strategy: histories to actions
⊨	U+22A8	Satisfaction	Truth at a state of the game structure
¬	U+00AC	Not sign	Negation
→	U+2192	Rightwards arrow	Material implication
q	—	State	A location of the concurrent game structure

Metatheory. Alur, Henzinger and Kupferman (2002) settled the complexity: ATL model checking is PTIME-complete and runs in time linear in the size of the game structure and of the formula, while ATL* model checking is 2EXPTIME-complete. Satisfiability is EXPTIME-complete for ATL (van Drimmelen 2003) and 2EXPTIME-complete for ATL* (Schewe 2008), so both are decidable. Taking A empty gives CTL's universal path quantifier and taking A to be the grand coalition gives the existential one, so ATL properly extends CTL, and ATL* properly extends ATL. Memoryless strategies suffice for ATL — a coalition able to enforce an ATL objective can do so with a strategy depending only on the current state — which is what makes the fixpoint algorithm linear; ATL* objectives genuinely require memory. Alternating bisimulation is the matching invariance notion, and Pauly's Coalition Logic is exactly the next-time fragment.

Applies to. Multi-agent systems. Game theory. Synthesis. Security protocols. Autonomous systems.

Limitations. The semantics assumes perfect information, and relaxing it breaks the theory rather than extending it: with imperfect information and perfect recall, ATL model checking is undecidable (Dima and Tiplea 2011), while the memoryless variant stays decidable but loses the fixpoint characterization that made the perfect-information case linear. The coalition modality quantifies over strategies existentially at each occurrence, so no formula can commit a coalition to a single strategy across nested modalities; recovering that requires strategy contexts or Strategy Logic, which gain the expressiveness, with non-elementary model checking and undecidable satisfiability. Coalitions are given, not formed: the language can say that a group is able to enforce an outcome but cannot say that its members would agree to, since it contains no preferences and no notion of rationality. Nothing quantitative is expressible — no probabilities, costs or payoffs — so equilibrium concepts lie outside it entirely.