GAMES RTN > Objectives

Objectives
Games and Automata for Synthesis and Validation

There is a growing need for formal methods that guarantee the reliability, correctness, and efficiency of computerised systems. This project adresses this challenge by developing specification and validation methodologies that are based on games and automata. Oriented at both foundational research and modern applications, this network aims to provide a novel set of techniques for the synthesis and validation of computing systems.

• Games provide a powerful mathematical framework with a well-developed theory as well as very general and versatile models of computation. In particular they capture in a natural way the aspect of interaction. Many synthesis and validation tasks, formula checking, or query evaluation problems can be formulated in game-theoretic terms. For instance, a software module can be understood as an agent playing a (possibly infinite) game with its environment according to a finite strategy. Accordingly, specifying a module amounts to formally describing a game, synthesizing a module amounts to computing a winning strategy and verifying a module against a specification amounts to checking that a strategy is winning.

• Automata provide a conceptually simple, yet general model for state-based information processing systems. Practical algorithms are often based on automata; in particular, automata based algorithms are used for highly efficient hardware verification tools. Further, automata theory is a well-developed discipline offering an enormous wealth of important results, relevant techniques, and well-explored connections to applications. In many cases, game-theoretic problems can be translated into algorithmic problems for automata.

Both concepts, automata and games, are intimately connected to logic, and have been used for a long time as tools for analysing the expressive power and the algorithmic properties of logical systems. Logical formulas can often be conveniently represented by automata, and evaluated by games. Systems and models can often be specified by automata and be analysed and compared by games. Recent research has demonstrated that games and automata, in combination with modal, temporal and fixed-point logics, are the basis of practically usable methods with industrial scale applications.

• A. Foundations: Games, automata, and logic. The combination of automata, game theory, and applied logic constitutes a powerful theory with important practical applications. However, the present state of the theory still has essential gaps in central issues.

  The precise interplay between automata, games, and logics is far from being understood. Structural properties of automata should be connected to syntactic conditions in specification logics, and the meaning of such properties or restrictions for algorithmic problems needs to be better investigated. A deeper integration of concepts from automata, games, and logics is needed for obtaining wider applications.

  A problem of crucial practical importance is the simplification or minimization of automata and games such that the infinite behaviour is preserved. Such minimization problems are well understood (and efficiently solvable) in the context of finite behaviour. A corresponding algorithmic theory for systems with infinite behaviour would mean a decisive step forward in our ability to handle large state-based systems.

  Some fundamental algorithmic problems are as yet unsettled. The most prominent one perhaps is the question whether parity games are solvable by a polynomial-time algorithm. In our network, the so far best available algorithms have been devised, and there is hope to completely solve this question; this would represent a breakthrough in our understanding of the verification problem.

• B. Reactive computation. This network wants to progress in a so-far unexploited potential of infinite games, namely to develop them as a model of reactive computation. Our aim is to devise methods for automatic synthesis of reactive controllers, extracted from the construction of winning strategies in infinite games. Based on recent progress made in our network, it seems now possible to isolate frameworks that are general enough for real applications but still permit efficient algorithmic solutions. A success in this direction would be a breakthrough analogous to the development of CTL-based model checking in the area of hardware verification.

  In current industrial software development, testing is the dominant form of validation and, despite it being an incomplete method, cannot always be replaced by formal verification. Testing can abstractly be viewed as a game, and we will use a game-based approach to develop the theoretical basis of testing reactive systems and tp derive criteria for comparing testing strategies.

• C. Verification: New Frontiers. Model checking and symbolic representation techniques have been applied with great success to hardware verification. One of the big challenges for the GAMES network is to extend this verification methodology so as to deal with broader classes of systems, including important classes of software systems. Different automata-based techniques have already been proposed for infinite state systems, but today's proposals can only be applied to simple scenarios and very rough abstractions of real software. It is essential to make current solutions more flexible and to deal with more expressive models.

  Another objective is to develop linear-time model checking technology. In spite of the phenomenal success of CTL-based model checking, its branching-time framework gives rise to several limitations. In contrast the linear-time framework is both expressive and intuitive, it supports compositional reasoning and semi-formal verification, and it is amenable to combining enumerative and symbolic search methods. It would be a practically important breakthrough to bring linear-time verification to an equally mature and robust technology as CTL-based verification. We can build now on solid automata-theoretic foundations for the linear-time framework, so that this is a realistic objective.

• D. Web Technologies: Queries and Protocols. Mobile Computing, e-Business and the World Wide 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, for instance concerning cryptographic protocols. The GAMES network will exploit the methodological proximity between databases and verification to develop game and automata based techniques for query evaluation and for the new validation tasks in this area. We want to represent protocol interaction by game models to obtain a powerful notion of security against adversaries, ranging from random noise to intelligent and hostile intruders. The ultimate goal is to have a ``CTL for protocols'', i.e., a logical specification language tailored for specifying protocol properties whose good algorithmic behavior makes it possible to answer questions about the security of a system by solving algorithmic problems about automata and games.

• Task 1: Minimizing automata and simplifying games. Algorithms for minimizing automata preserving their infinite behaviour will be designed and analysed. An algebraic approach to automata on (game) trees will be developed, modular and hierarchical decomposition of games, and methods for simplifying games will be studied. To make automata-based methods more practical, efficient on-the-fly constructions of automata will be developed.
• Task 2: Algorithmic analysis of parity games. The main goal is to determine whether winning positions and winning strategies for parity games can be computed in polynomial time. Another goal is the analysis, improvement and implementation of practical (possibly incomplete) algorithms for solving parity games. Finally this work will be exploited for applications in logic and verification.
• Task 3: Synthesis and testing for reactive computation. The participants will study classes of games for which the strategy synthesis problem is solvable (at least in principle), isolate cases where the controller synthesis problem admits efficient solutions and develop concrete algorithms. A game-based testing methodology for reactive systems will be developed.
• Task 4: Analysis techniques for infinite-state systems. To extend algorithmic approaches to synthesis, verification, and testing beyond the scope of the existing validation techniques and tools the GAMES network will develop automata-based analysis techniques for infinite-state systems. This includes
  • symbolic representation strutures (based on automata and logic) for manipulating infinite sets of states,
  • analysis procedures based on these representation structures for different models of infinite-state systems (such as timed models and parametrized networks with an arbitrary number of components connected according to different topologies).
• Task 5: Linear-time model checking. The participants will develop theory, algorithms, and methodologies to make linear time a viable framework for model-checking technology, complementing the branching time framework. Algorithms and methodologies that are proven analytically and/or experimentally to be effective will be embodied into prototype tools to facilitate technology transfer.
• Task 6: Game models for protocols. Multiparty games with incomplete and uncertain information as models of protocols will be developed. Games with cooperating players will serve as tools for validating protocols for client-server database systems, more complicated scenarios of games with hostile players, uncertainty and infinite state spaces will be used for analysing cryptographic protocols.
• Task 7: Logics, games, and efficient query evaluation. Game-theoretic techniques will be used to attack unresolved problems of expressiveness, such as fixed point hierarchies and the associated algorithmic questions. Model checking games will be used for efficient formula evaluation with applications to verification and query evaluation. The network will develop algorithms and perform systematic complexity and scalability studies for query evaluation, concentrating on structural properties of data that have been shown to significantly reduce query complexity.
• Task 8: Automata and query languages for semistructured data. A new approach to data on the web based on a new notion of automata, similar to tree automata, will be developed. On the practical side, automata concepts will be combined with database methods for analysing and improving existing XML query languages and automatic information extractors. We will also use verification techniques based on automata and logics for validating and comparing Document Type Definitions (DTDs). aspect and the practical impact of the network.
• Task 9: Accessibility and dissemination. To be of practical use on a large scale, automata and game based methods must become more known and more accessible to non-experts. Besides training events on specific aspects and applications of automata and games, the network will make efforts to provide an accessible and unified treatment of this methodology.