Model checking games

Erich Grädel

(Aachen)

Model checking problems ("is a given formula true in a given structure?") for almost every logic can be cast as strategy problems ("which player does have a winning strategy in a given game?") for the appropriate evaluation games (also called Hintikka games).

In games for first-order logic, all plays are finite and the strategy problem can be solved in linear time in the size of the game graph. For fixed point logics, the appropriate evaluation games are parity games, which admit also infinite plays. Each position is assigned a priority, and the winner of an infinite play is determined according to whether the least priority seen infinitely often during the play is even or odd.

Infinite games are also important for other applications. They model in a natural way the non-terminating interaction of a reactive system with its environment: the specification of a reactive system can be seen as a winning condition in a game, and a reactive program that fulfills the specification implements a winning strategy. Parity games are especially interesting because on one side, they are powerful enough to simulate large classes of games and, on the other side they admit positional winning strategies.

An polynomial time algorithm for computing winning sets and winning strategies of parity game would also provide a solution for the model checking problem for the modal mu-calculus, and vice versa. While we do not know whether this is possible in general, we can analyze the structure of parity games and isolate `easy' cases that admit efficient solutions. We link these `easy games' to logic and thus obtain efficient model checking algorithms for fragments of fixed point logic.
Thursday 8th May 2003, 14:00
Robert Recorde Room
Department of Computer Science