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