Game Development Reference

In-Depth Information

player, the Falsifier, attempts to refute this. In contrast to common definitions

of the meaning of logical formulae which proceed bottom-up, from atomic

formulae through the application of logical operators (such as connectives

and quantifiers) to more complicated ones, game-theoretic semantics proceed

top-down. Starting with a complicated sentence, Verifier and Falsifier try to

justify their claims by moves to supposedly simpler assertions. By playing

such an evaluation game the two players thus produce a sequence of formulae

that ends when they reach an atomic statement, which cannot be simplified

further. The Verifier has succeeded to justify her original claim if the atomic

formula reached at the end of the sequence of is true, and Falsifier has won

if it is false. We thus assume that the truth of atomic statements can be

readily determined, for instance by a look-up in a table.

model-checking games permit us to evaluate logical formulae by solving

algorithmic problems on games
such as the computation of
winning

regions
and the construction of
winning strategies
. For the most common

logical systems, such as
first-order logic
(FO) or
propositional modal

logic
(ML), the construction of the associated model-checking games is

straightforward, and the games are simple in several senses. First of all, the

goals of the players are the simplest conceivable objectives in such games,

namely
reachability objectives
: each player tries to force the play to a

terminal position where she has won (like check mate). Secondly, it is the

case that in each move, the formula is strictly simplified, so that every play

terminates after a number of moves that is bounded by the nesting depth of

logical operators in the formula. In particular there are no infinite plays, and

this holds no matter whether the structure on which the formula is evaluated

is finite or infinite. Finally, in the case of finite game graphs, the winner

of such a reachability game can be determined in linear time (with respect

to the size of the game graph). Thus, algorithms for solving reachability

games can be applied to evaluate first-order formulae, and give us a detailed

complexity analysis for the model-checking problem of first-order logic on

finite structures.

But life is not always that simple. For expressing properties of finite

structures, and for defining combinatorial problems on classes of structures

(such as graphs), first-order logic is rather limited. For many tasks arising

in computer science there is thus a need of other kinds of logical systems,

such as temporal logics, dynamic logics, game logics, transitive closure logics,

fixed-point logics and so on, which extend a basic formalism like FO and ML

by more powerful operators.

The natural model-checking games for such logics are more complicated

than reachability games. In particular, they admit infinite plays. Essential

Search Nedrilad ::

Custom Search