Alternating-Time Temporal Logic

Definition

Alternating-Time Temporal Logic is a temporal logic for reasoning about what coalitions of agents can force in concurrent game models.

Why It Matters

ATL makes strategic ability a first-class modal operator. That makes it useful for specifying multi-agent tasks, verifying coalitional safety/liveness properties, and connecting strategic specifications to learning or model synthesis.

Formalism / Key Objects

• A typical strategic modality is <<C>>X phi, meaning coalition C has a strategy to make phi true in the next state.
• Other standard forms include <<C>>F phi for eventual enforceability, <<C>>G phi for invariance, and <<C>> phi U psi for until goals.
• ATL is interpreted on concurrent game models with states, agents, actions, transition functions, and valuations.
• Hybrid ATL adds nominals and @_alpha phi, allowing formulas to refer to named states.
• ATL Model Building extends this picture with LAMB update operators that alter the game model itself.

Connections

• Strategic Reasoning uses ATL to express coalition abilities rather than merely possible paths.
• Varricchione2023 - Synthesising Reward Machines for Cooperative MARL uses ATL task specifications to synthesize cooperative reward machines.
• Galimullin2025 - Changing the Rules of the Game extends ATL to reason about dynamic model updates.
• Probabilistic Strategic Timed CTL is an adjacent branching-time strategic logic with probabilities and real-time bounds.

Common Confusions

• ATL’s <<C>> is not an existential path quantifier; it quantifies over strategies for a coalition against possible choices of others.
• A coalition ability claim depends on the underlying game model and strategy assumptions.
• Updating a model can change whether an ATL formula is true even if the formula itself is unchanged.

Key Sources

• Galimullin2025 - Changing the Rules of the Game
• Varricchione2023 - Synthesising Reward Machines for Cooperative MARL