18.211 Automaten, Logiken und unendliche Spiele

2st. Do 10 - 12 C-221
(Hauptstudiumsschwerpunktvorlesung im WiSe 2004/2005)

Achtung: Beginn der Vorlesung ab 28.10. erst um 10:30 Uhr

Lernziel:

Kennenlernen von Methoden zur
- Modellierung
- Verifikation
- Model-Checking von reaktiven Systemen.

Es werden folgende Themen ausführlich behandelt:
- Automaten auf unendlichen Wörtern
- Bisimulation
- Unendliche Spiele
- Modaler μ-Kalkül

Weiterhin wird auf folgende verwandte Formalismen eingegangen:
- Bewachte Logiken als entscheidbare Erweiterungen modaler Logiken
- Automaten und monadische Logik zweiter Stufe

Inhalt:

Die Theorie der Automaten auf unendlichen Folgen (ω-Wörtern) und unendlichen Bäumen ist die Grundlage für die Modellierung, Analyse und Synthese reaktiver (nichtterminierender) Systeme; viele Algorithmen für die automatische Verifikation (Model-Checking) benutzen Konstruktionen und Ergebnisse dieser Theorie. Daneben spielt diese Theorie eine wichtige Rolle bei Entscheidbarkeitsfragen und Komplexitätsuntersuchungen in der mathematischen Logik.

In den letzten Jahren sind eine Reihe wichtiger Fortschritte in diesem Bereich der Automatentheorie erzielt worden. Hier geht es zum Beispiel um Anwendungen alternierender Automaten, um Verbindungen zur Theorie unendlicher Spiele (effektive Konstruktion von Gewinnstrategien), um Model-Checking-Probleme für unendliche Transitionssysteme sowie um Zusammenhänge zwischen der monadischen Logik zweiter Stufe und dem modalen μ-Kalkül.

Stellung im Studienplan:

Hauptstudium, Vertiefungsgebiete P10, P2, P3, P4, P5, P6, Th1, Th2, Th3, Th4; Schwerpunkte SEM, SV, VIS, WV

Voraussetzungen:

Grundstudium, Vorlesung AUK (oder TGP) empfohlen

Vorgehen:

Vorlesung
(als theoretische Vertiefung (nach PO'85) geeignet, insbesondere auch für viele P-Gebiete)
auch für individuelle "Theorie-Schwerpunkte" (nach PO'98)

Literatur:

Erich Grädel, Wolfgang Thomas, Thomas Wilke (Hrsg.), "Automata, Logics, and Infinite Games", LNCS 2500, Springer-Verlag, 2002

Wolfgang Thomas, "Automata on Infinite Objects." In: J. van Leeuwen, Hrsg., Handbook of Theoretical Computer Science, Bd. B (Formal Methods and Semantics), Amsterdam: Elsevier, 1990, S. 134-191.

Wolfgang Thomas, "Languages, Automata and Logic." In: A. Salomaa, G. Rozenberg, Hrsg., Handbook of Formal Languages, Bd. 3 (Beyond Words), Berlin: Springer, 1997, S. 389-455.

Periodizität:

einmalig

Eignung:

Bedingt geeignet für Lehramtsstudierende, Nebenfachstudierende, Bioinformatikstudierende, Wirtschaftsinformatikstudierende.

Stichwörter:

Logiken, Spezifikation, Verifikation, ω-Automaten, Spiele, Model-Checking