Book contents
- Frontmatter
- Contents
- List of contributors
- Preface
- 1 A Primer on Strategic Games
- 2 Infinite Games and Automata Theory
- 3 Algorithms for Solving Parity Games
- 4 Back and Forth Between Logic and Games
- 5 Turn-Based Stochastic Games
- 6 Games with Imperfect Information: Theory and Algorithms
- 7 Graph Searching Games
- 8 Beyond Nash Equilibrium: Solution Concepts for the 21st Century
- Index
4 - Back and Forth Between Logic and Games
Published online by Cambridge University Press: 01 June 2011
- Frontmatter
- Contents
- List of contributors
- Preface
- 1 A Primer on Strategic Games
- 2 Infinite Games and Automata Theory
- 3 Algorithms for Solving Parity Games
- 4 Back and Forth Between Logic and Games
- 5 Turn-Based Stochastic Games
- 6 Games with Imperfect Information: Theory and Algorithms
- 7 Graph Searching Games
- 8 Beyond Nash Equilibrium: Solution Concepts for the 21st Century
- Index
Summary
Abstract
In this chapter we discuss relationships between logic and games, focusing on first-order logic and fixed-point logics, and on reachability and parity games. We discuss the general notion of model-checking games. While it is easily seen that the semantics of first-order logic can be captured by reachability games, more effort is required to see that parity games are the appropriate games for evaluating formulae from least fixed-point logic and the modal µ-calculus. The algorithmic consequences of this result are discussed. We also explore the reverse relationship between games and logic, namely the question of how winning regions in games are definable in logic. Finally the connections between logic and games are discussed for more complicated scenarios provided by inflationary fixed-point logic and the quantitative µ-calculus.
Introduction
The idea that logical reasoning can be seen as a dialectic game, where a proponent attempts to convince an opponent of the truth of a proposition is very old. Indeed, it can be traced back to the studies of Zeno, Socrates, and Aristotle on logic and rhetoric. Modern manifestation of this idea are the presentation of the semantics of logical formulae by means of model-checking games and the algorithmic evaluation of logical statements via the synthesis of winning strategies in such games.
model-checking games are two-player games played on an arena which is formed as the product of a structure and a formula ψ where one player, called the Verifier, attempts to prove that ψ is true in while the other player, the Falsifier, attempts to refute this.
- Type
- Chapter
- Information
- Lectures in Game Theory for Computer Scientists , pp. 99 - 145Publisher: Cambridge University PressPrint publication year: 2011
- 5
- Cited by