Game Logic

Origin. Rohit Parikh introduced propositional game logic (1985). Builds on dynamic logic, adding game-theoretic operations. Models strategic interaction where outcomes depend on choices of multiple agents. Connects logic, game theory, and verification. Extended by various researchers for different game-theoretic concepts.

Models. Games as first-class logical objects. Programs in dynamic logic are one-player games against nature. Game logic adds two-player (or multi-player) games where outcome depends on both players' strategies. "Player 1 has a strategy to achieve φ regardless of Player 2's moves." Models strategic ability, not just temporal possibility.

Formalism.

Two-player determined games: Players: Angel (∃, trying to achieve φ) and Demon (∀, trying to prevent φ).

Game operations (Parikh):

γ₁ ∪ γ₂ — Angel chooses between γ₁ and γ₂
γ₁ ∩ γ₂ — Demon chooses between γ₁ and γ₂
γ₁ ; γ₂ — play γ₁ then γ₂
γ* — repeat γ (Angel decides when to stop)
γᵈ — dual: swap Angel and Demon roles
φ? — test: proceed if φ, else fail

Game modalities:

⟨γ⟩φ — Angel has a strategy in game γ to reach a state satisfying φ
[γ]φ — all plays of γ end in φ (Demon can't avoid φ)

Duality: [γ]φ ≡ ¬⟨γ⟩¬φ

Relationship to dynamic logic: Dynamic logic = game logic where all choices are Angel's. Game logic adds Demon choices (∩) and dualization (γᵈ).

Determined games: In a determined game, either Angel or Demon has a winning strategy. ⟨γ⟩φ ∨ ⟨γᵈ⟩¬φ

Examples:

⟨a ∪ b⟩φ: Angel can achieve φ by choosing a or b
⟨a ∩ b⟩φ: Angel can achieve φ regardless of whether Demon picks a or b
⟨(a ∩ b)*⟩φ: Angel can eventually achieve φ despite Demon's interference

Symbols.

Symbol	Unicode	Name	Meaning
⟨γ⟩	U+27E8/9	Diamond	Angel can achieve
[γ]	—	Box	All plays lead to
∪	U+222A	Angel choice	Angelic nondeterminism
∩	U+2229	Demon choice	Demonic nondeterminism
;	—	Sequence	Sequential composition
*	—	Iteration	Repeated game
ᵈ	—	Dual	Swap players
?	—	Test	Conditional

Metatheory. Propositional game logic is EXPTIME-complete (same as PDL). Determined games: every game formula is equivalent to one without duals. Game logic = μ-calculus fragment (alternation depth 1). Complete axiomatization exists. Game semantics provides models: strategies, winning conditions.

Applies to. Multi-agent systems. Verification of reactive systems (controller vs environment). Synthesis (constructing winning strategies). Security (attacker vs defender). Planning against adversaries.

Limitations. Two-player assumption; multi-player requires coalition logic. Determined games only; some real games aren't determined. Perfect information assumed; imperfect information is harder. Strategies are implicit; extracting them requires additional work. The logic describes what's achievable, not how to achieve it.