Infinite two-person games provide a natural model for non-terminating reactive systems. Not only synthesis and validation of reactive programmes, but also many other tasks arising in the construction and verification of computing systems, can be solved via the construction of winning strategies in games. GAMES is an ESF research networking programme that develops the algorithmic theory of infinite games and provides game-based formal verification methods.
A simple model of infinite games where two players move a token along the edges of a graph and thus produce an infinite path, has turned out to be extremely useful in numerous applications, ranging from the synthesis of reactive controllers to the evaluation of logical formulae and database queries, and the verification of formal specifications written in temporal logics. Such a game is specified by a game graph (the arena of the game) and a winning condition that singles out those infinite plays that are won by the first player (the others are won by the opponent). Infinite games of this form have a long tradition in mathematics. The classical theory of infinite games, as developed in descriptive set theory, links determinacy of games—the question of whether one of the two players has a winning strategy—with the topological properties of the winning conditions. However, the classical theory does not have an algorithmic content and studies different questions to the algorithmic theory of infinite games being developed in computer science.
The importance of games for computer science comes from the fact that games capture in a natural way the aspect of interaction. Infinite games, as described above, model in a faithful way reactive programmes that are characterised by their nonterminating behaviour and perpetual interaction with their environment. In this framework, a software module can be understood as an agent playing an infinite game against its environment according to a finite strategy. Thus, specifying a module amounts to formally describing a game, synthesising a module amounts to computing a winning strategy, and verifying a module against a specification amounts to checking that a strategy is indeed a winning strategy. For the theory of infinite games as it is used in computer science, algorithmic aspects are obviously of central importance. It is not sufficient to know that a winning strategy exists. Instead, we are interested in efficient constructions of a winning strategy and in minimising the complexity of the strategy itself.
The algorithmic theory of infinite games is intimately connected to two other fields—automata theory and logic. Automata provide a conceptually simple yet general model for state-based information processing systems. Logical systems (in particular modal and temporal logics) are used for the specification of the desired non-terminating behaviour of a system and the winning condition of the associated game. Logical formulae can often be conveniently represented by automata and evaluated using games. Recent research has demonstrated that games and automata, in combination with modal, temporal, and fixed-point logics, are the basis of practical methods with industrial-scale applications.