Vorlesung: Automatentheorie und Formale Sprachen, Wintersemester 13/14
 

Dozent: Ralf Möller

Ort: TUHH SBS95 H0.03

Zeit: Mon. 15:45 - 17.15

Voraussetzungen:

Diskrete Algebraische Strukturen, Graphentheorie und Optimierung, Computational Logic, Prozedurale Programmierung, Software Engineering

Sprache:

Bilingual: Deutsch/Engslish
Einige Vorlesungen werden in Deutsch, einige in Englisch abgehalten, so dass die Studierenden auch an die englische Nomenklatur herangeführt werden.

Inhalt:

Wir erarbeiten die wesentlichen Modelle für Automaten und Formalen Sprachen mit direktem Anwendungsbezug. Dabei betrachten wir als Anwendungen den Compilerbau, die Verifikation digitaler Systeme sowie die Definition einfacher paralleler Verarbeitungseinheiten (z.B. UML-Aktivitätaendiagramme) und stellen dabei Querbezüge zu Grammatiken und zur Logik her.

  1. Einführung
    Motivation, Deterministische Endliche Automaten, Definition und Konstruktion
  2. Reguläre Sprachen, Abschlusseigenschaften
    Wortproblem, String Matching
  3. Nichtdeterministische Automaten
    Rabin-Scott-Transformation von nichtdeterministischen in deterministische Automaten
  4. e-Automaten, Minimierung von Automaten
    Eliminierung von e-Kanten, Eindeutigkeit des Minimierungsergebnisses (modulo Zustandsumbenennung)
  5. Myhill Nerode Theorem
    Beweis der Korrektheit des Minimierungsverfahrens, Äquivalenzklassen von Strings induziert durch Automaten
  6. Pumping Lemma für reguläre Sprachen
    Bereitstellung eines Werkzeugs, mit dem man zeigen kann, dass ein endlicher Automat nicht ausdrucksstark genug sein kann, um ein Wortproblem zu lösen
  7. Regluläre Ausdrücke vs. Automaten
    Äquivalenz von Formalismen, Systematische Modelltransformationen, Reduktionen
  8. Kellerautomaten und kontextfreie Grammatiken
    Definition von Kellerautomaten, Grammatikdefinition, Ableitung, Parsebaum, Mehrdeutigkeit, Pumping Lemma für kontextfreie Grammatiken, Transformation von Formalismen: Von Kellerautomaten zu Grammatiken und zurück
  9. Chomsky-Normalform
  10. CYK-Algorithmus zur Entscheidung des Wortproblems für kontextfreie Grammatiken
  11. Deterministische Kellerautomaten
  12. Deterministische vs. Nichtderministische Kellerautomaten
    Parsing-Anwendungen: LL(k), LR(K)-Parser bzw. -Grammatiken, LR(1)-Grammatiken vs. deterministische Kellerautomaten, Compiler-Compiler
  13. Reguläre Grammatiken
  14. Ausblick: Turing-Maschinen und linear beschränkte Automaten vs. allgemeine und Kontextsensitive Grammatiken
    Chomsky-Hierarchie
  15. Mealy- und Moore-Automaten
    Automaten mit Ausgaben (und ohne Endzustände), unendliche Zustandsfolgen, Automatennetze
  16. Omega-Automaten: Automaten über unendlichen Eingabeworten, Büchi-Automaten
    Repräsentation von Zustandssystemen und Anwendungen zur Verifikation mit Hilfe von Modallogik-Spezifikationen (insbesondere LTL)
  17. LTL-Safety-Bedingungen und Model-Checking mit Büchi-Automaten
    Zusammenhang zwischen Automaten und Logik
  18. Andere Akzeptanzbedingungen, Alternierung als Erweiterung zum Nichtdeterminismus, Alternating Automata, Tree Automata, Alternating Tree Automata (ATAs)
    ATA Model-Checking von CTL und CTL*
  19. Fixpunkte, Aussagenlogisches mu-Kalkül
  20. Charakterisierung von regulären Sprachen durch Monadische Logik Zweiter Ordnung (Monadic Second Order Logic, MSO)
  21. Reasoning about knowledge
    Modal logics about knowledge

Danksagung

Die Vorlesung verwendet Material aus dem Buch von Vossen/Witt und insbesondere die PPT-Folien hierzu von Thomas Ottmann (Freiburg). In der Einleitung sind Folien von Christian Sohler (Dortmund) eingearbeitet. Weiterhin habe ich einige PPT-Präsentationen von Lenore Blum (CMU) für den Kurs 15-453 FORMAL LANGUAGES, AUTOMATA, AND COMPUTABILITY verwendet. Teile 12-15 sind aus Präsentationen von Costas Busch, damals RPI, übernommen. Folien wurden übernommen von Igor Potapov (Liverpool) und Chang-Beom Choi. Der Algorithmus zur Umrechnung von LTL-Formeln in Büchi-Automaten wurde von Ingo Weigelt (Düsseldorf) dargestellt. ATAs werden unter Verweis auf Präsenationen von Marsha Chechik (Univ. ov Toronto) eingeführt. Ich bedanke mich bei den Autoren, dass sie ihr PPT- und PDF-Material im Web für Lehrzwecke bereitgestellt haben.

Hinweise auf die Originalautoren sind in den hier verfügbar gemachten Dokumenten eingearbeitet.

Literatur/Skript:

Alte Klausuren finden Sie hier
Ralf Möller