Research
Infinite Graphs / Verification of Infinite Systems using Model Checking
Automatic verification of state-based systems was inititally developed for systems with finite state-space. We contribute to the research in order to extend this method to infinite systems. For this purpose, classes of infinite graphs that can be finitely represented are studied.
Problems concerning this topic are also investigated in the project Finitely Represented Infinite Graphs - Structure, Behaviour, Algorithmics.
Papers on this: [Löd02a], [Löd02b], [Cac03], [CW03], [Tho03a], [WT04], [Kar05a].
Generalized Automata Theory
Concerning the application of automata theory (especially when it comes to modelling of computer-systems and program verification) more general automata models than the one of finite automata over finite words are necessary. This generalization can concern the automata models considered as well as the structure that is treated by these. In our research group we examine e.g. automata over trees, graphs (matrices of letters), partial orders and general relational structures.
Papers on this: [MST02], [Tho03b], [ATW03], [KT04], [Kar04], [Kar05a].
Infinite Games and Synthesis of Reactive Programs
Infinite two-player-games are, on the one hand, a natural model for non-terminating reactive systems, on the other hand, they are an approach to many problems of model checking. One central problem is the automated controller synthesis (that means implementation of winning strategies). Besides this there are also applications in classical logic. Our research has the following objectives:
- develop winning strategies for games over finite state-space (automated synthesis of controllers that are optimal concerning different criteria).
- develop algorithmic procedures with which it is possible to generate winnning strategies also for games over infinite state-space.
Some selected papers on this: [Tho97d], [Vög00], [Cac02b], [Cac03b], [WHT03], [Wal03], [BSL04].
Automata and Logic Systems, Automata on Infinite Words
The importance of automata theory for verification is based on the fact that automata are a linking part between system description and specification. This is due to the fact that logic-systems can be translatedinto automata (e.g. temporal logic, modal logic, program logic). The exact knowledge of this relation between logic and automata is the basis of progress in algorithmic verification. Since the applications in general concern non-terminating reactive systems, automata on infinite words (and infinite trees, respectively) are a vital subject matter of this research.
Papers on this: [Tho90a], [Tho99a], [LT00], [CT02].
Software Tools on Automata Theory
The following tools have been developed by the research group:
- AMoRE - basic algorithms for regular languages including the algebraic theory of regular languages;
- OMEGA - platform for the testing of automata theoretic algorithms in the theory of infinite games (finished);
- GASt - Platform for algorithms to solve infinite two-player games and to determinise Büchi automata.
Several Diploma Theses treat the extension of these tools: A Java-interface for AMoRE, graphical components for AMoRE, an extension on tree automata, etc.
Papers on this: [SV00b], [MMP+95].