Logik in der Informatik Prof. Dr. Nicole Schweikardt

In diesem Logbuch werden regelmäßig Informationen bereit gestellt. Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden.

1. Fr, 19.04.2024:
   • Eröffnungsveranstaltung. Klärung von Organisatorischem (entlang der Webseite der Vorlesung). Abschnitt 1.1 (Wdh. Formale Sprache und reguläre Ausdrücke)

   Material:

   • Folien 1--21
   • Skript 1--15

2. Di, 23.04.2024:
   • Abschnitt 1.2 Begrifflichkeiten rund um endliche Automaten. Beginn mit dem Kapitel 2: Probleme endlicher Automaten auf endlichen Worten: Leerheitsproblem (inkl. Beweis), Wortproblem und Sprachendlichkeitsproblem (inkl. Beweisidee), Universalitätsproblem (inkl. Beweis)

   Material:

   • Folien 22--39
   • Skript 15--28

   Ergänzende Lektüre, in der Sie bei Interesse weiterlesen können (aber nicht müssen):

   • Sanjeev Arora and Boaz Barak: Computational Complexity: A Modern Approach [Link]

3. Fr, 26.04.2024:
   • Probleme endlicher Automaten auf endlichen Worten: Heute Inklusions- und Äquivalenzproblem. Neuer Abschnitt: Logik und Automaten: Wiederholung Grundbegriffe Logik erster Stufe (speziell auf Wortstrukturen),Beweis (aa)+ ist nicht FO-defbar, einführendes Beispiel für Intuition MSO.

   Material:

   • Folien 40--60
   • Skript 29--40

   Ergänzende Lektüre, in der Sie bei Interesse weiterlesen können (aber nicht müssen):

   • Henrik Björklund et al.: Logik und Automaten: ein echtes Dreamteam [Link]

4. Fr, 03.05.2024:
   • Syntax und Semantik von MSO auf Wortstrukturen, BET-Theorem (Beweis -> LuK), Entscheidbarkeit von Erfüllbarkeitsproblem und Äquivalenzproblem auf Wortstrukturen mittels Automaten gezeigt, model checking problem, Zitat von Meyer & Stockmeyer, Syntax und Semantik SFR, Satz von McNaughton und Papert [Theorem 2.31] (Bweis -> LuK), nicht-zählende reguläre Sprachen, sowie Syntax und Semantik von LTL auf Wortstrukturen inkl. Erweiterung unseres Theorems 2.31 und Beweis (sternfrei regulär => nicht zählend)

   Material:

   • Folien 61--80
   • Skript 41--52

5. Di, 07.05.2024:
   • Beweis LTL => FO, Sternhöhe (verallgemeinerter) regulärer Ausdrücke, Feedbackzahl endl. Automaten.
     Neuer Abschnitt: Minimierung von Automaten: NFA-Homomorphismen, Wdh. Äquivalenzrelationen und Partionierungen, Quotientenautomat, DFA-Homomorphismus, Kongruenz, Quotienten-DFA

   Material:

   • Folien 80--94
   • Skript 52--64

   Ergänzende Lektüre, in der Sie bei Interesse weiterlesen können (aber nicht müssen):

   • J.-É. Pin et al.: Some results on the generalized star-height problem [Link]

6. Fr, 17.05.2024:
   • Beweis L(A) =L(A_/~A); Minimierung von DFA: Myhill-Nerode-Äquivalenz, kanonischer Automat, Beweis L=(A_L), Index eine ÄR, Zusammenhang zw. Index der Nerode-ÄR und regulären Sprachen, Isomorphie minimaler DFA, Algorithmus zur Berechnung der kan. Kongruenz

   Material:

   • Folien 95--105
   • Skript 64--72

7. Di, 21.05.2024:
   • Beispiellauf des Algo. 1; Minimierung von NFA: Minimierung als Entscheidungsproblem (inkl. Beweis PSPACE-Härte), Bisimulationsspiel und der dazugehörigen Qutientenautomat; Das syntaktische Monoid: Monoid(Def.), Homomorphismen über Monoiden, Satz (Zhg reguläre Sprachen und enld. Monoid, bisher ohne Beweis)

   Material:

   • Folien 105--116
   • Skript 72--83

   Ergänzende Lektüre, in der Sie bei Interesse weiterlesen können (aber nicht müssen):

   • Berstel et al.: Minimization of Automata. [Link]

8. Fr, 24.05.2024:
   • Satz (Zhg reguläre Sprachen und endl. Monoid) inkl. Beweis, Transitionsmonoid, das syntaktische Monoid in zwei äquivalenten Def. (inkl. Beweis der Äquivalenz), syntaktische Kongruenz, Gruppenfreiheit von Monoiden und der Satz von Schützenberger (ohne Beweis), Anwendungen an Bsp.
     Neuer Abschnitt: Alternierende Automaten, Def inkl positiv Boole'schen Formeln und deren Semantik, Lauf und Sprache von AFAs, erstes Beispiel

   Material:

   • Folien 116--127
   • Skript 83--91

9. Di, 28.05.2024:
   • Bsp. AFA als kompakte Repräsentanten reg. Sprachen. Dualer AFA. Satz und Beweis zu NFA -> AFA und AFA -> NFA, gedächtnislose Läufe von AFA.
     Neuer Abschnitt: Lernen regulärer Sprachen: Angluin's scenario, erster naiver Ansatz, Angluin's Lernalgorithmus am Beispiel, dabei Definition des observation table, dessen Vollständigkeit und Konsitenz, Hypothese-DFA.

   Material:

   • Folien 128--138
   • Skript 91--105

10. Fr, 31.05.2024:
    • Angluin's Lernalgorithmus terminiert und Laufzeit in Anzahl der Fragen.
      Neuer Abschnitt:Automaten mit Ausgabe. Moore Automat, Mealy Automat und deren Äquivalenz (inkl. konstruktivem Beweis)
      Neues Kapitel: Endliche Automaten auf endlichen Bäumen. Abschnitt Bäume: Einführende Beispiele, Alphabet mit Rang, zwei äquivalente Def. von Σ-Bäumen; DbuTA, Akzeptanz und Sprache

    Material:

    • Folien 138--151
    • Skript 106--118

11. Di, 4.06.2024:
    • Höhe von Σ-Bäumen, Beispiele für von einem DbuTA akzeptierte Baumsprachen, Def.: reguläre Baumsprachen; Zhg. Ableitungsbäume kontextfreier Grammatiken und reg. Baumsprachen; Abschlußeigenschaften reg. Baumsprachen; Bsp. einer nicht regulären Baumsprache; Pumping Lemma und Beispielanwendung; NbuTA; Ausdrucksstärke NbuTA vs. DbuTA; NtdTA, DtdTA: Ausdrucksstärke NbuTA vs. NtdTA, Ausdrucksstärke NtdTA vs. DtdTA; Myhill/Nerode-Äquiv., Bspe;

    Material:

    • Folien 150--166
    • Skript 118--130

12. Fr, 7.06.2024:
    • Satz und Beweis: Baumsprache ist regulär gdw. der Index ~_T endlich; Algo. Berechnung aller errichbaren Zustände eine NbuTA, dmit: Leerheitsproblem entscheidbar; Kor.: Universalitätsproblem-, Inklusions- und Äquivalenzproblem entscheidbar für NbuTA und DbuTA; Minimierung von DbuTA; Eindeutigkeit des minimalen DbuTA;
      Reguläre Ausdrücke; Definition der Verkettung und des Kleene-Stars für Baumsprachen Satz: Baumsprache regulär gdw. definierbar durch reg. Ausdruck (Beweis offen)

    Material:

    • Folien 167--176
    • Skript 131--139

13. Fr, 14.06.2024:
    • Beweis zu Satz: Baumsprache regulär gdw. definierbar durch reg. Ausdruck; Neuer Abschnitt: MSO, Σ-Bäume als Strukturen, MSO und FO auf Baumstrukturen, Beispiele, Satz von Doner, Thatch-Wright inkl. Beweisidee von Automaten zur Logik, T_even ist FO-defbar auf Σ=Σ₀ ∪ Σ₂ mit Σ₀={a} und Σ₂={f}.

    Material:

    • Folien 176-181
    • Skript 139-149

14. Di, 18.06.2024:
    • Abschluss von Kapitel 3: Satz über sternfreie Baumsprachen und anti-chain Logik, Anwendung für Alphabete der Form Σ=Σ₀ ∪ Σ₂; Alphabete ohne Rang: Σ-beschriftete Bäume, NuTA, Normalform und DuTA, Determinisierung, fcns-Kodierung, Zusammenhang mit regulären Baumsprachen, Korollar zur Entscheidbarkeit des Leerheits,- Inklusions,- und Äquivalenzproblems für NuTA; TWA: Def. & Arbeitsweise, Abschluss unter Schnitt und Vereinigung, Zusammenhang (n)TWA und reguläre Baumsprachen (ohne Beweis) und Hinweis bzgl. Ausdrucksstärke von deterministischen vs. nichtdeterministischen TWA.

    Material:

    • Folien 182-198
    • Skript 149-160

    Ergänzende Lektüre, in der Sie bei Interesse weiterlesen können (aber nicht müssen):

    • Mikołaj Bojańczyk: Tree-walking automata. [Link]

15. Fr., 21.06.2024:
    • Neues Kapitel 4: Abschnitt 1: unendliche Wörter und Sprachen: Def. ω-reguläre Sprachen, Abschluss unter Vereinigung und Linkskonkatenation, Büchi-Automaten (NBA und DBA), deterministische vs nicht-deterministische BA, Hilfslemmas für den Satz v. Büchi, Satz von Büchi , Schnitt von BA (mit Hilfe des Satzes von Büchi), Müller-Automaten (MA), Umwandlung MA in NBA

    Material:

    • Folien 199-211
    • Skript 161-171

16. Di., 25.06.2024:
    • Umwandlung MA in NBA (Korrektheit der Konstruktion), Umwandlung DBA zu MA, Abschlusseigenschaften MA, Rabin-Automat (RA), Umwandlung RA zu MA und zurück, Abschlusseigenschaften RA, Streett-Automat (DSA), Umwandlung DSA zu MA, RA zu DSA (wobei DSA Komplemtentsprache spricht, Gleichmächtigkeit v. Ausdrucksstärke MA, RA, DSA in Theorem zusammengefasst. Abschlusseigenschaften DSA, Determinisierung - warum Potenzmengenkonstruktion allein nicht hilft, Safra-Bäume, Safra-Konstruktion (Def)

    Material:

    • Folien 211-223
    • Skript 172-182

17. Fr., 28.06.2024:
    • Safra-Konstruktion: Beispiel, McNaughton's Theorem, Vollständigkeit und erster Teil der Korrektheit.

    Material:

    • Folien 224-227
    • Skript 183-192

18. Di., 02.07.2024:
    • Safra-Konstruktion: Abschluss der Korrektheit. Komplementierung Büchi-Automat. Leerheitsproblem, Äquivalenzproblem & Univeralitätsproblem für Büchi-Automaten.
      Kapitel 5: unendliche Bäume, nichtdeterministische Baum-Automaten mit Büchi-, Müller- und Paritätsakzeptanzbedingung, Büchi vs. Müller

    Material:

    • Folien 228-237
    • Skript 192-204

19. Fr., 05.07.2024:
    • Paritätsbaumautomaten vs. Müllerbaumautotan, dafür: LAR-Konstruktion; Komplementierung von Paritätsbaumautomaten mit Hilfe von Paritätsspielen

    Material:

    • Folien 238-244
    • Skript 204-211

20. Di., 09.07.2024:
    • reguläre Bäume, eingabefreier Paritätsbaumautomat, Leerheitsproblem für Paritätsautomaten. Über- und Ausblick

    Material:

    • Folien 244-248
    • Skript 211-215