Contact People Projects Teaching Publications Intranet
 

Vorlesung: Automatentheorie und Formale Sprachen, Wintersemester 11/12
 

Dozent: Ralf Möller

Die Uebung wird betreut von Karsten Martiny

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 oder Google-Map-Reduce-Repräsentationen) 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. Beweistechniken mit nichtdeterministischen Automaten
    Abschlusseigenschaften
  5. e-Automaten, Minimierung von Automaten
    Eliminierung von e-Kanten, Eindeutigkeit des Minimierungsergebnisses (modulo Zustandsumbenennung)
  6. Myhill Nerode Theorem
    Beweis der Korrektheit des Minimierungsverfahrens, Äquivalenzklassen von Strings induziert durch Automaten
  7. Pumping Lemma für reguläre Sprachen
    Bereitstellung eines Werkzeugs, mit man zeigen kann, dass ein endlicher Automat nicht ausdrucksstark genug sein kann, um ein Wortproblem zu lösen
  8. Regluläre Ausdrücke vs. Automaten
    Äquivalenz von Formalismen, Systematische Modelltransformationen, Reduktionen
  9. Kellerautomaten und kontextfreie Grammatiken
  10. Chomsky-Normalform
  11. CYK-Algorithmus zur Entscheidung des Wortproblems für kontextfreie Grammatiken
  12. Deterministische Kellerautomaten
  13. Deterministische vs. Nichtderministische Kellerautomaten
    Parsing-Anwendungen: LL(k), LR(K)-Parser bzw. -Grammatiken, LR(1)-Grammatiken vs. deterministische Kellerautomaten, Compiler-Compiler
  14. Reguläre Grammatiken
  15. Ausblick: Turing-Maschinen und linear beschränkte Automaten vs. allgemeine und Kontextsensitive Grammatiken
    Chomsky-Hierarchie
  16. Mealy- und Moore-Automaten
    Automaten mit Ausgaben (und ohne Endzustände), unendliche Zustandsfolgen, Automatennetze
  17. Omega-Automaten: Automaten über unendlichen Eingabeworten, Büchi-Automaten
    Repräsentation von Zustandssystemen und Anwendungen zur Verifikation mit Hilfe von Modallogik-Spezifikationen (insbesondere LTL)
  18. LTL-Safety-Bedingungen und Model-Checking mit Büchi-Automaten
    Zusammenhang zwischen Automaten und Logik
  19. Andere Akzeptanzbedingungen, Alternierung als Erweiterung zum Nichtdeterminismus, Alternating Automata, Tree Automata, Alternating Tree Automata (ATAs)
    Alternating Automata als Modell für die Spezifikation von Cloud-Computing-Jobs (z.B. Googles Map-Reduce) oder BPEL-Geschäftsprozesse
    ATA Model-Checking von CTL und CTL*
  20. Fixpunkte, Aussagenlogisches mu-Kalkül
  21. Ausblick auf die Vertiefungsveranstaltungen: Symbolisches Model-Checking, Symbolisches Rechnen auf Automaten, Ordered Binary Decision Diagrams (OBDDs), Minterme, Partial-Order Reduction, Monadic Second-Order Logic (MSO), MSO definability vs. Büchi definability, reguläre Sprachen, Untere Schranken: Ehrenfeucht-Fraïssé-Spiele (als Ergänzung zu den Pumping-Lemmata), FO-Definability, sternfreie Sprachen

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

Ralf Möller