Die Forschungsthemen und -projekte des Lehrstuhls für Informatik 7 werden auf der Webseite des Lehrstuhls unter "Forschung/Projekte" und "Diplomarbeiten" erläutert.
In der Diplomprüfung Informatik wird das Vertiefungsfach "Automaten, Logik und Verifikation" geprüft. Prüfer für dieses Vertiefungsgebiet ist Prof. Dr. Wolfgang Thomas. Es werden regelmäßig Vorlesungen aus der folgenden Liste angeboten. Änderungen werden sich eventuell mit Einführung des Masterstudiengangs Informatik ergeben (voraussichtlich WS 2008/2009).
Diese Theorievorlesung bietet zunächst eine Einführung in die Theorie der Automaten auf unendlichen Wörtern. Das zentrale Anwendungsgebiet ist die Analyse und Synthese von "reaktiven Systemen". Dies sind Systeme wie beispielsweise Controller und Kommunikationsprotokolle, die zwei wichtige Eigenschaften aufweisen: Sie terminieren typischerweise nicht, und sie stehen in ständiger Interaktion mit ihrer Umgebung.
Der Fokus des ersten Teils der Vorlesung liegt auf der Spezifikation von nicht-terminierendem Verhalten. Hierfür werden endliche Automaten benutzt, die unendliche Wörter akzeptieren. Viele Ergebnisse der Automatentheorie für endliche Wörter lassen sich auf den Fall unendlicher Wörter übertragen, allerdings sind hierfür komplexere Konstruktionen nötig. Vorgestellt werden auch die Verbindung von Automaten zu logischen Systemen und die Methode des "Model-Checking", der algorithmischen Verifikation von zustandsbasierten Systemen.
Im zweiten Teil der Vorlesung wird die Interaktion zweier Parteien in reaktiven Systemen behandelt: Abstrakt gesehen sind "Programm" und "Umgebung" die beiden Spieler in einem unendlichen Zweipersonen-Spiel. Die Konstruktion eines Programms kommt dann der Konstruktion einer Gewinnstrategie gleich. Es wird gezeigt, wie Gewinnstrategien in unendlichen Spielen gefunden werden können, wenn der Zustandsraum des betrachteten Systems endlich ist.
In dieser Theorievorlesung werden grundlegende Begriffsbildungen und Ergebnisse der Automatentheorie vorgestellt, die in der Systemkonstruktion und -analyse benötigt werden. Die Vorlesung gliedert sich in zwei große Teile. Im ersten Teil werden endliche Automaten auf Wörtern und Bäumen betrachtet. Themenstichworte sind:
Der zweite Teil befasst sich mit Erweiterungen von endlichen Automaten zur Modellierung und Analyse von unendlichen Systemen. Die wesentlichen Stichworte für diesen Teil sind:
Die Vorlesungen 1. und 2. wurden von 2004 bis 2006 auch in jeweils zwei
"Halbvorlesungen" (V2 + Ü1) angeboten:
Die Rekursionstheorie ist die Theorie des absolut Berechenbaren. Sie wurde durch Gödel, Church, Kleene, Turing und Post begründet und führt mit relativ kurzen Schlüssen zu weitreichenden Einsichten.
Zur Illustration ein Beispiel: Ein Saboteur will durch einen Algorithmus jedes C-Programm P so ändern, dass das entstehende Programm P' etwas anderes leistet als P. Wie kann er das erreichen?
Ein Hauptsatz der Rekursionstheorie besagt, dass der Saboteur sein Vorhaben nicht verwirklichen kann, egal welchen Sabotage-Algorithmus er benutzt. Die eleganten Begriffe und Schlüsse der Rekursionstheorie haben für andere Disziplinen als Vorbild gedient, vor allem für die Komplexitätstheorie. Wir geben eine Einführung in die elementaren Begriffe und Sachverhalte der Rekursionstheorie. Voraussetzung ist die Grundvorlesung "Berechenbarkeit und Komplexität" des Grundstudiums.
Stichworte zum Inhalt:
Die regulären und die kontextfreien Sprachen lassen sich nach Kriterien von "Schwierigkeit" klassifizieren, z.B. nach Definierbarkeit mit speziellen regulären Ausdrücken, Grammatiken, Logikformeln oder auch Schaltkreisen. Ziel der Vorlesung ist die Einführung in diese Klassifikationstheorie, die mathematische Eleganz mit interessanten Anwendungen (z.B. in der Verifikation) verbindet. Zudem fließen hier Ansätze aus der Automatentheorie, der Logik, der Algebra und der Komplexitätstheorie zusammen.
Stichworte sind:
(seit 2005 in Abstimmung mit Lehrstuhl für Informatik 2)
Model-Checking ist eine Methode zur automatischen Verifikation von Software und Hardware. Wir geben eine Einführung in mehrere Ansätze: Begriffliche Grundlagen, temporale Logiken LTL und CTL, Model-Checking-Verfahren, Komplexitätsfragen, Ausblick in symbolische Verfahren (OBDD's) und die Verifikation von Realzeit-Spezifikationen (timed systems).
(gemeinsam mit der Gruppe "Mathematische Grundlagen der Informatik")
Für Diplomanden, Mitarbeiter und weitere Interessierte. Nähere Informationen sind auf der Webseite der Arbeitsgemeinschaft verfügbar.