Game Development Reference
In-Depth Information
4
Back and Forth Between Logic and Games
Erich Gradel
RWTH Aachen University
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.
4.1 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
A
A
while the other
Search Nedrilad ::




Custom Search