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