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	Strategic ability
○	U+25CB	Next	One step
□	U+25A1	Always	Invariant
◇	U+25C7	Eventually	Reachability

Metatheory. Model checking: linear time for ATL (PTIME-complete), 2EXPTIME-complete for ATL* (Alur, Henzinger, and Kupferman 2002). Satisfiability: EXPTIME-complete for ATL, 2EXPTIME-complete for ATL*. Synthesis connection. Alternating bisimulation is the right invariance notion. Decidable.

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

Limitations. Perfect information assumed. Memory requirements. Coalition formation not modeled. Incomplete information variants complex.