The research topics and projects of the Chair for Computer Science 7 are described on the chair's webpage under "Research/Projects" and "Diploma Theses". The area of specialisation for the diploma examination in computer science is "Automata, Logic and Verification". Prof. Dr. Wolfgang Thomas is the examiner. The chair offers courses from the list below on a regular basis. There may be changes due to the introduction of the Master program in computer science (presumably winter term 2008/2009).
This course first offers an introduction to the theory of automata on infinite words. The central application area is the analysis and synthesis of "reactive systems". These are systems such as controllers and communication protocols, in which two features are essential: Usually they do not terminate, and they are in continuous interaction with their environment.
In the first part of the course we concentrate on the specification of non-terminating behaviour. For this purpose one uses finite automata which accept infinite words. Many results of the theory of automata on finite words can be transferred to the case of infinite words, but more complex constructions are necessary. We also present the connection between automata and logical systems and introduce the method of "model-checking", the algorithmic verification of state-based systems.
The second part of the course deals with the interaction between two parties in reactive systems: In an abstract sense, "program" and "environment" are the players in an infinite two-person game. Program construction then amounts to the construction of a winning strategy. We show how to find winning strategies in infinite games when the state space of the system under consideration is finite.
In this course, fundamental concepts and results from automata theory are presented that are needed for constructing and analyzing systems. The course is divided in two main parts. In the first, finite automata on words and trees are considered. Some of the topics covered are the following:
In the second part of the course, extensions of finite automata for modelling and analyzing infinite systems are considered. The main topics covered in this part are:
Between 2004 and 2006, the above courses 1. and 2. have also been given
as two split-up courses each (V2 + Ü1):
Recursion theory is the "theory of the computable". It was established by Gödel, Church, Kleene, Turing and Post and allows for deeper insight with relatively short arguments.
As an illustrative example, consider a saboteur who wants to change every C-program P by an algorithm in such a way that the resulting program P' has a behaviour different from P. How can he achieve this?
A fundamental theorem of recursion theory states that the saboteur cannot achieve his goal, no matter what sabotage algorithm he uses. The elegant concepts and conclusions of recursion theory have served as a role model for other fields of research, especially for complexity theory. The course offers an introduction to the fundamental concepts and results of recursion theory. Knowledge from the undergraduate course "Berechenbarkeit und Komplexität" is required.
Topics covered comprise:
Regular and context-free languages can be categorized according to criteria of "difficulty", e.g. by definability with special regular expressions, grammars, logic formulas or circuits. The course offers an introduction to this theory of classification, which combines mathematical elegance and interesting applications (e.g. in verification). Furthermore, approaches from automata theory, logic, algebra, and complexity theory are connected.
Topics covered comprise:
(as of 2005 in coordination with the Chair for Computer Science 2)
Model Checking is a method to automatically verify software and hardware. The course offers an introduction to several approaches, covering conceptual fundamentals, the temporal logics LTL and CTL, model checking techniques, complexity issues, a brief introduction of symbolic methods (OBDDs), and the verification of timed specifications.
(together with the research group "Mathematical Foundations of Computer Science")
For master students (diplomands), members of staff and other interested persons. For further information, please see the webpage of the Research Seminar.