| |
Games and Automata for Synthesis and Validation
by Erich Grädel
Infinite two-person games provide a natural model for non-terminating reactive systems. Not only synthesis and validation of reactive programs, 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 a European research training network 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, 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 programs 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 with 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. 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 by 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.
GAMES (Games and Automata for Synthesis and Validation) is a European Research Training Network that includes research groups from seven European universities (Aachen, Bordeaux, Edinburgh, Paris, Uppsala, Vienna, Warsaw) and one university from the USA (Rice). The goal of the network is to develop the algorithmic theory of infinite games and to provide specification and validation methodologies based on the interplay of automata theory, mathematical logic, and infinite games. More specifically, the research objectives are the following:
- Foundations: games, automata, and logic: The combination of infinite games with automata theory and applied logic constitutes a mathematical theory with enormous potential for practical applications. To exploit this potential, challenging problems concerning the mathematical foundations of infinite games and the interplay between automata, games, and logics must be solved and a deeper integration of concepts from automata, games, and logics is needed.
- Reactive computation: The network wants to exploit the potential of infinite games as a model of reactive computation and to devise game-based methods for the automatic synthesis and testing of reactive controllers.
- Verification: New Frontiers. Model-checking techniques have been applied with great success to the verification of hardware. One of the big challenges for this network is to extend the verification methodology so as to deal with broader classes of systems, including important classes of software systems.
- Web technologies: queries and protocols: Mobile computing, e-Business, and the Web have dramatically changed the way in which data are stored and manipulated. New technologies have emerged, with a strong demand for better foundations and efficient algorithmic strategies, and with new validation and security problems. The GAMES-network develops automata- and game-based techniques for query evaluation and the new validation tasks in this area.
Link:
http://www.games.rwth-aachen.de
Please contact:
Erich Grädel, RWTH Aachen, Germany
Tel: +49 241 8021730
E-mail: graedel informatik.rwth-aachen.de
|
