Baumautomaten und Anwendungen

» Diese Veranstaltung wird auf deutsch gehalten.

Vorlesung im Wintersemester 2004/2005

ArtTermine/OrtBeginnVeranstalter
V2 Di 10:00 - 11:30 AH VI 12.10.2004 Thomas, Löding
Ü1 Mi 16:00 - 16:45 AH II 20.10.2004 Löding, Rohde

Inhalt

Endliche Automaten auf unendlichen Bäumen werden bei der Analyse nichtterminierender Systeme benötigt, deren Läufe verzweigen (wie zum Beispiel in allen reaktiven Systemen, in denen auf Eingaben der Umgebung reagiert wird). Algorithmen über Baumautomaten bilden z.B. die Grundlage für viele Model-Checking-Verfahren.

Stichworte zur Gliederung der Vorlesung:
  1. Einführung und Motivation
  2. Büchi-Baumautomaten
  3. Anwendung auf Entscheidbarkeit von Programmlogiken (z.B. PDL)
  4. Muller-, Paritäts- und Rabin-Baumautomaten, unendliche Spiele und das Komplementproblem
  5. Anwendungen in klassischer und temporaler Logik (S2S, CTL*)
  6. Anwendungen in der Synthese von Controllern

Vorkenntnisse

Diese Vorlesung wendet sich an Studierende ab dem 5. Fachsemester. Kenntnisse aus der Grundstudiumsvorlesung "Automatentheorie und formale Sprachen" werden vorausgesetzt.

Kombination mit anderen Veranstaltungen Diese Vorlesung kann mit der Vorlesung "Automaten auf unendlichen Wörtern" (W. Thomas) zu einer vierstündigen Veranstaltung (V4, Ü2) kombiniert werden. In dieser Kombination entspricht der Stoff in etwa dem Inhalt der Vorlesung "Automata and Reactive Systems" vom WS 2002/03.

Wichtiger Hinweis: Die beiden Vorlesungen werden separat behandelt. Die Kriterien für die Ausgabe von Übungsscheinen sind unabhängig für beide Vorlesungen. Bei Erfüllung der Kriterien werden kleine Übungsscheine (V2, Ü1) ausgegeben. Dann und nur dann, wenn man beide kleinen Übungsscheine erhalten hat, kann man diese gegen einen großen Übungsschein (V4, Ü2) eintauschen.

Prüfungsleistung

Um einen Übungsschein (V2, Ü1) zu bekommen, müssen die beiden folgenden Bedingungen erfüllt werden:

  1. Es muss eine bestimmte Anzahl an Punkten in den Übungen erreicht werden (ca. 50%). Dabei zählen nur die Aufgaben zu Vorlesung "Baumautomaten und Anwendungen", nicht die Aufgaben der anderen Vorlesung.
  2. Die Abschlussklausur muss bestanden werden.

Wer genügend Punkte in den Übungen erreicht hat, aber die Abschlussklausur nicht mitgeschrieben oder nicht bestanden hat, ist zur Teilnahme an einer Nachprüfung berechtigt.

Wer nicht genügend Punkte in den Übungen erreicht hat, kann die Abschlussklausur mitschreiben, aber er oder sie erhält auch bei Bestehen der Klausur keinen Übungsschein.