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. - Einführung Motivation, Deterministische Endliche Automaten, Definition und Konstruktion - Reguläre Sprachen, Abschlusseigenschaften Wortproblem, String Matching - Nichtdeterministische Automaten Rabin-Scott-Transformation von nichtdeterministischen in deterministische Automaten - e-Automaten, Minimierung von Automaten Eliminierung von e-Kanten, Eindeutigkeit des Minimierungsergebnisses (modulo Zustandsumbenennung) - Myhill Nerode Theorem Beweis der Korrektheit des Minimierungsverfahrens, Äquivalenzklassen von Strings induziert durch Automaten - 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 - Regluläre Ausdrücke vs. Automaten Äquivalenz von Formalismen, Systematische Modelltransformationen, Reduktionen - Kellerautomaten und kontextfreie Grammatiken - Chomsky-Normalform - CYK-Algorithmus zur Entscheidung des Wortproblems für kontextfreie Grammatiken - Deterministische Kellerautomaten - Deterministische vs. Nichtderministische Kellerautomaten Parsing-Anwendungen: LL(k), LR(K)-Parser bzw. -Grammatiken, LR(1)-Grammatiken vs. deterministische Kellerautomaten, Compiler-Compiler - Reguläre Grammatiken - Ausblick: Turing-Maschinen und linear beschränkte Automaten vs. allgemeine und Kontextsensitive Grammatiken Chomsky-Hierarchie - Mealy- und Moore-Automaten Automaten mit Ausgaben (und ohne Endzustände), unendliche Zustandsfolgen, Automatennetze - Omega-Automaten: Automaten über unendlichen Eingabeworten, Büchi-Automaten Repräsentation von Zustandssystemen und Anwendungen zur Verifikation mit Hilfe von Modallogik-Spezifikationen (insbesondere LTL) - LTL-Safety-Bedingungen und Model-Checking mit Büchi-Automaten Zusammenhang zwischen Automaten und Logik - Andere Akzeptanzbedingungen, Alternierung als Erweiterung zum Nichtdeterminismus, Alternating Automata, Tree Automata, Alternating Tree Automata (ATAs) ATA Model-Checking von CTL und CTL* - Fixpunkte, Aussagenlogisches mu-Kalkül - Charakterisierung von regulären Sprachen durch Monadische Logik Zweiter Ordnung (Monadic Second Order Logic, MSO)