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
ε	U+03B5	Epsilon	Tolerance in an ε-optimal strategy
π	U+03C0	Pi	A path through the game structure
∃	U+2203	Existential quantifier	Quantification over coalition strategies
∀	U+2200	Universal quantifier	Quantification over resulting paths
⊨	U+22A8	Double turnstile	Satisfaction at a state or on a path
Act	—	Actions	Move set

Metatheory. Alur, Henzinger, and Kupferman (2002) proved ATL model checking over concurrent game structures PTIME-complete and linear in the product of the structure and the formula, while ATL* is 2EXPTIME-complete for model checking and satisfiability alike. Turn-based games embed as the special case in which every agent but one has a single available action at each state, so concurrent structures strictly generalize them — and the generalization costs determinacy. With pure strategies concurrent games are not determined even for reachability objectives, since neither player can commit first; determinacy is recovered only by randomization, and Martin (1998) proved Blackwell determinacy for Borel payoffs, giving every such game a value. Optimal strategies need not exist even then: de Alfaro, Henzinger, and Kupferman (1998) showed concurrent reachability games in which a player has ε-optimal strategies for every ε but no optimal one, and where winning with probability one requires unbounded memory.

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. The linear-time model checking result is measured against a structure whose transition function is indexed by joint actions, so its size is already exponential in the number of agents — the complexity is favourable only relative to an input that itself blows up. Determinacy fails for pure strategies, so the logic's existential strategy quantifier does not partition the states into winning regions for the two sides as it does in turn-based games. Perfect information and synchronous rounds are built into the definition; imperfect information with perfect recall makes model checking undecidable, and asynchrony needs a different structure altogether. ATL has no probabilities and no preferences, so Nash equilibrium is not expressible in it and requires Strategy Logic, at non-elementary cost. Continuous action spaces are outside the framework.