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.

Metatheory. The semantics is monotone neighbourhood semantics: each game term denotes an effectivity function assigning to every state the sets of outcomes Angel can force, and the dual γᵈ is the pointwise dual of that function, which is why the determinacy schema ⟨γ⟩φ ∨ ⟨γᵈ⟩¬φ holds by construction rather than by a theorem. Duals can be pushed inward until they apply only to atomic games, but they cannot be eliminated. Satisfiability is EXPTIME-complete: hardness comes from PDL, which is the dual-free and ∩-free fragment, and membership from the faithful embedding into the modal μ-calculus, itself EXPTIME-complete by Emerson and Jutla. The embedding is not into any bounded fragment — Berwanger (2003) showed game logic spans the whole alternation hierarchy. Parikh's 1985 axiomatization was finally proved complete by Enqvist, Hansen, Kupke, Marti and Venema (2019).

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

Limitations. Games are two-player and zero-sum by construction: the dual operator presupposes that whatever Angel cannot force Demon can, so non-zero-sum interaction and any third player fall outside the language, and determinacy is imposed by the semantics rather than established of the games modelled. Perfect information is likewise assumed; the effectivity functions are defined on states, so a player who cannot distinguish two states has no representation. Only forcing is expressible, never preference, so no equilibrium notion and no notion of rational play can be stated. Strategies are quantified away inside the modality and never appear as objects, so a proof that ⟨γ⟩φ holds does not by itself yield the strategy. And because game logic occupies the whole μ-calculus alternation hierarchy, translation-based tools inherit the worst case rather than a bounded fragment's better behaviour.

© 2026 Lingenic LLC