Automaten auf Unendlichen Wörtern

» Diese Veranstaltung wird auf deutsch gehalten.

Vorlesung im Wintersemester 2004/2005

ArtTermine/OrtBeginnVeranstalter
V2 Mo 15:00 - 16:30 AH V 18.10.2004 Thomas
Ü1 Mi 17:00 - 17:45 AH II 20.10.2004 Thomas, Rohde

Inhalt

Endliche Automaten auf unendlichen Wörtern (omega- Automaten) sind das zentrale Hilfsmittel bei der formalen Analyse nichtterminierender Systeme (etwa zur Prozessverwaltung und Steuerung von Anlagen). Die Ergebnisse der vorgestellten Theorie werden in der automatischen Verifikation und Synthese solcher Systeme eingesetzt.

Im Zentrum stehen die logischen und algorithmischen Eigenschaften der omega-Automaten. Stichworte zur Gliederung der Vorlesung:

  1. Büchi-Automaten
  2. Deterministische omega-Automaten
  3. Akzeptierbedingungen und die Klassifikation von omega-Sprachen
  4. Anwendungen in Logik und Verifikation

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 "Baumautomaten und Anwendungen" (C. Löding) 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 "Automaten auf unendlichen Wörtern", 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.