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:* ATL + past + strategy quantification. More expressive, higher complexity.

Symbols.

Metatheory. Model checking: PTIME (ATL), EXPTIME (ATL*). Synthesis connection. Bisimulation for ATL. 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.

© 2026 Lingenic LLC