Algorithmische Automatentheorie WS24/25

News

• 1. Oktober: Die erste Vorlesung findet am Montag, den 21. Oktober statt.
• 4. Dezember: Zusätzlicher Hintergrund zu Parikhs Theorem
• 11. Dezember: Korrektur des Verma Seidl Schwentick Beweis

Organisation

• Der Modulverantwortliche ist Prof. Dr. Roland Meyer.
• Die Vorlesung wird von Prof. Dr. Roland Meyer mit Unterstützung von Jens Gutsfeld (jens-oliver.gutsfeld@tu-braunschweig.de) gehalten.
• Die große Übung wird von Anton Opaterny (anton.opaterny@tu-braunschweig.de) gehalten.
• Vorlesungstermine: Montag 15:00 - 16:30, Dienstag 13:15 - 14:45 in IZ 358.
• Große Übung: Mittwoch, 13:15 - 14:45 in IZ 358.
• Abgabe der Übungsblätter per Mail an anton.opaterny@tu-braunschweig.de.

Modul

Um das Modul erfolgreich abzuschließen, sind zwei Leistungen zu erbringen:

• Prüfungsleistung: Sie bestehen die (vorraussichtlich) mündliche Abschlussprüfung.
• Studienleistung: Sie erreichen mindestens 50% der Punkte in den Übungsaufgaben.

Inhalt

• Finite state systems
  • Büchi automata
  • MSO and Büchi's theorem
  • LTL and Presburger arithmetic
• Recursive programs
  • Pushdown automata, pre* and post*
  • Bounded context switching
  • Tree automata, Rabin's theorem
• Parameterised systems
  • Regular model checking
  • LTL(MSO)
  • Quotients, abstraction, and extrapolation