README⤓ .txt 2026-07-17T121634.146 000000000000752 Logics whose semantics or subject matter is strategic interaction: systems in which truth, provability, or meaning is cast as the existence of a winning strategy, and logics for reasoning about games, strategies, and coalitions. Games serve here both as a semantic tool and as an object of formal theory.
Banach-Mazur Games⤓ .md 2026-08-19T214615.000 000000000016704 Banach and Mazur (1930s), Oxtoby (1957). Infinite games on topological spaces. Players choose nested sets. Winning = nonempty intersection. Foundation for descriptive set theory.
Borel Determinacy⤓ .md 2026-08-19T214552.000 000000000019384 Martin (1975). Infinite games with Borel winning sets are determined. One player has winning strategy. Beyond Borel: requires large cardinals. Foundation for descriptive set theory.
Buchi Automata⤓ .md 2026-07-16T012319.000 000000000038864 J. Richard Büchi, "On a decision method in restricted second order arithmetic" (1962), which introduced ω-automata to prove S1S decidable; Rabin (1969) extended it to trees and S2S; McNaughton (1966) gave the determinization. Vardi and Wolper's "An automata-theoretic approach to automatic program verification" (1986) turned the theorem into the technology every model checker runs on.
Coalition Logic⤓ .md 2026-08-19T214508.000 000000000029784 Marc Pauly developed coalition logic (2000, 2002). Extends modal logic to reason about what groups of agents can achieve. Alternating-time Temporal Logic (ATL) by Alur, Henzinger, and Kupferman (1997, 2002) combines coalition power with temporal logic. Foundation for multi-agent system verification.
Concurrent Game Logic⤓ .md 2026-07-15T060304.000 000000000021392 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.
Dialogical Logic⤓ .md 2026-07-15T211301.000 000000000014792 Lorenzen, Lorenz (1960s). Erlangen school. Game semantics. Dialogue games. Foundation of constructive semantics.
Dynamic Logic⤓ .md 2026-08-19T185927.000 000000000027736 Vaughan Pratt introduced dynamic logic in 1976 ("Semantical considerations on Floyd–Hoare logic"), reading programs as modalities. Fischer and Ladner isolated the propositional fragment PDL, combining modal logic with regular expressions over programs, and settled its complexity (1977, 1979). David Harel developed the first-order theory (1979). Foundational for program verification and reasoning about actions.
Ehrenfeucht-Fraisse Games⤓ .md 2026-07-15T065144.000 000000000015216 Ehrenfeucht (1961) building on Fraïssé (1954). Game characterization of elementary equivalence. Spoiler vs Duplicator. n-round game captures n-quantifier equivalence.
Extensive Game Logic⤓ .md 2026-07-15T235628.000 000000000019232 Bonanno's modal logic of extensive games (2001, 2002); Harrenstein, van der Hoek, Meyer, and Witteveen on game-theoretic reasoning in modal logic (2002, 2003); van Benthem's "Games in dynamic-epistemic logic" (2001) and Logic in Games (2014). Logic for extensive form games. Tree-structured games with perfect/imperfect information. Epistemic reasoning about game positions. Backward induction, subgame perfection.
Game Logic⤓ .md 2026-08-19T185927.000 000000000026792 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.
Game Semantics⤓ .md 2026-07-15T061325.000 000000000020848 Lorenzen's dialogical logic (1960s). Hintikka's game-theoretic semantics (1970s). Abramsky, Jagadeesan, Malacaria: full abstraction (1990s). Games between Proponent (verifier) and Opponent (falsifier). Foundation for programming language semantics.
Ludics⤓ .md 2026-07-15T063259.000 000000000017992 Girard introduced ludics (2001). Foundation for logic via interactive games. Designs as basic objects, not formulas. Orthogonality defines behavior/type. Unifies logic, computation, and game semantics. "Logic from interaction."
Mechanism Design Logic⤓ .md 2026-07-15T063454.000 000000000019600 Connects mechanism design (Hurwicz, 1960s) to logic. Pauly's coalition logic. Van der Hoek, Wooldridge: social choice in logic. Formal verification of mechanisms. Automated mechanism design foundations.
Modal Mu-Calculus⤓ .md 2026-08-19T232002.000 000000000030120 Dana Scott and Jaco de Bakker used fixed points in program semantics (1969); Park (1969, 1976) on fixpoint induction. Dexter Kozen, "Results on the propositional μ-calculus" (1983), gave the system and its axiomatization; Walukiewicz (1995) proved completeness. The modal mu-calculus combines modal logic with fixed-point operators. Subsumes CTL, LTL, PDL in expressive power. Foundation for model checking algorithms (OBDD-based, game-based).
Parity Games⤓ .md 2026-07-15T065146.000 000000000015248 Emerson and Jutla (1991). Two-player infinite games on graphs. Parity condition on infinite plays. Decides μ-calculus satisfiability. Positional strategies suffice.
Sabotage Game Logic⤓ .md 2026-07-15T061942.000 000000000017784 Extends sabotage logic to full game-theoretic setting. Van Benthem's sabotage games (2002). Combines sabotage with game logic and ATL-style reasoning. Multi-agent adversarial graph modification. Strategic reasoning under sabotage.
Signaling Game Logic⤓ .md 2026-07-15T062737.000 000000000018344 Lewis's signaling games (1969). Spence's signaling (economics, 1973). Game-theoretic semantics of communication. Logic for strategic information transmission. Foundation for pragmatics and mechanism design.
Strategy Logic⤓ .md 2026-07-15T055419.000 000000000025216 Krishnendu Chatterjee, Thomas Henzinger, and Nir Piterman introduced Strategy Logic (SL, 2007, 2010). Extends ATL with explicit strategy quantification. Strategies are first-class objects: quantify over them, bind them to agents. More expressive than ATL* but with higher complexity. Foundation for advanced multi-agent verification.
CRITERIA⤓ .txt 2026-07-15T162259.000 000000000007288 Not sufficient: A logic that merely admits a game-theoretic model without games as its content. A probabilistic decision framework (Probabilistic).