Concurrent Game Logic

Origin. Alur, Henzinger, and Kupferman introduced concurrent game structures (1997-2002). Agents act simultaneously rather than taking turns. Generalizes turn-based games to concurrent moves. ATL and ATL* designed for this setting. Models reactive systems with simultaneous interaction.

Models. Simultaneous moves by multiple agents. Turn-based: one agent moves, then another. Concurrent: all agents choose actions simultaneously. Outcome depends on joint action profile. Models real-time systems, protocols, and environments.

Formalism.

Concurrent game structure: G = (Ag, S, s₀, Act, d, δ, L) where:

Ag = {1,...,n}: agents
S: states, s₀: initial state
Act: action set
d: S × Ag → 2^Act (available actions)
δ: S × Act^n → S (transition given joint action)
L: S → 2^AP (labeling)

Strategy: σᵢ: S⁺ → Act (history-dependent) or σᵢ: S → Act (memoryless/positional)

Outcome: out(s, σ_A) = paths from s when coalition A plays σ_A Against all possible strategies of opponents Ag\A.

ATL semantics on concurrent games: s ⊨ ⟨⟨A⟩⟩φ iff ∃σ_A.∀π ∈ out(s, σ_A). π ⊨ φ

Key difference from turn-based: Multiple agents choose simultaneously. No agent sees others' current choice. Information is symmetric (all see same state).

Nash equilibrium: Strategy profile where no agent benefits from deviating. Expressible in Strategy Logic, not in ATL.

Symbols.

Symbol	Unicode	Name	Meaning
⟨⟨A⟩⟩	—	Coalition can	A can ensure
[[A]]	—	Coalition must	A cannot avoid
∥	U+2225	Simultaneous	Concurrent actions
σ	U+03C3	Strategy	Action choice function
out	—	Outcome	Possible paths
δ	U+03B4	Transition	Next state
Act	—	Actions	Move set

Metatheory. ATL model checking on concurrent games is PTIME. ATL* is 2EXPTIME-complete. Strategy synthesis is PTIME for memoryless ATL. Concurrent games strictly generalize turn-based. Reduction: turn-based embeds as special case. Partial observation adds complexity (undecidable in general).

Applies to. Multi-agent system verification. Protocol analysis. Reactive synthesis (against environment). Distributed systems. Security (attacker-defender games). Resource competition. Real-time system modeling.

Limitations. Perfect information assumption strong. Continuous action spaces not handled. Probabilistic extension (PATL) less developed. Large joint action space explosion. Strategy representation can be exponential. Assumes synchronous rounds (async is harder).