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. Di, 15.04.2025:
   • Eröffnungsveranstaltung: Einführung ins Thema, 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, 22.04.2025:
   • 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 Zugehörigkeit; Härtebeweis angefangen)

   Material:

   • Folien 22--38
   • Skript 15--27

   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, 25.04.2025:
   • Probleme endlicher Automaten auf endlichen Worten: Heute Abschluss Härtebeweis Universalität, Inklusions- und Äquivalenzproblem. Neuer Abschnitt: Logik und Automaten: Wiederholung Grundbegriffe Logik erster Stufe (speziell auf Wortstrukturen), Beweis (aa)+ ist nicht FO-defbar.

   Material:

   • Folien 38--58
   • Skript 27--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. Di, 06.05.2025:
   • Einführendes Beispiel für Intuition; MSO: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] (Beweis -> LuK), nicht-zählende reguläre Sprachen; Erweiterung unseres Theorems 2.31 und Beweis (sternfrei regulär => nicht zählend)

   Material:

   • Folien 59--75
   • Skript 40--51

5. Fr, 09.05.2025:
   • 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. Di, 13.05.2025:
   • 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; Beispiellauf des Algo.;

   Material:

   • Folien 95--107
   • Skript 64--74

7. Fr, 16.05.2025:
   • Minimierung von NFA: Minimierung als Entscheidungsproblem (inkl. Beweis PSPACE-Härte), Bisimulationsspiel und der dazugehörigen Quotientenautomat; Das syntaktische Monoid: Monoid(Def.), Homomorphismen über Monoiden, Satz (Zhg reguläre Sprachen und endl. Monoid, inkl. Beweis), Transitionsmonoid, das syntaktische Monoid in zwei äquivalenten Def. (inkl. Beweis der Äquivalenz)

   Material:

   • Folien 105--123
   • Skript 72--86

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

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

8. Di, 20.05.2025:
   • Gruppenfreiheit von Monoiden und der Satz von Schützenberger (ohne Beweis), Anwendungen am Bsp. sternfreier regulärer Sprachen
     Neuer Abschnitt: Alternierende Automaten, Def inkl positiv Boole'schen Formeln und deren Semantik, Lauf und Sprache von AFAs, 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.

   Material:

   • Folien 123--134
   • Skript 86--98

9. Fr, 23.05.2025:
   • 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 Konsistenz, Hypothese-DFA.
     Neuer Abschnitt: Automaten mit Ausgabe. Moore Automat, Mealy Automat und deren Äquivalenz (inkl. konstruktivem Beweis)
     

   Material:

   • Folien 134--146
   • Skript 98--112

10. Di, 27.05.2025:
    • 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, 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;

    Material:

    • Folien 146--164
    • Skript 113--128

11. Di, 3.06.2025:
    • NtdTA, DtdTA: Ausdrucksstärke NbuTA vs. NtdTA, Ausdrucksstärke NtdTA vs. DtdTA; Myhill/Nerode-Äquiv., Bspe; 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: regAusdruck -> Automat, Rückrichtung offen)

    Material:

    • Folien 164--181
    • Skript 128--141

12. Fr, 6.06.2025:
    • Beweis zu Satz: Baumsprache regulär gdw. definierbar durch reg. Ausdruck: Rückrichtung;
      Neuer Abschnitt: MSO, Σ-Bäume als Strukturen, MSO und FO auf Baumstrukturen, Beispiele, Satz von Doner, Thatch-Wright inkl. Beweisidee von Automaten zur Logik für ein Beispielalphabet, T_even ist FO-defbar auf Σ=Σ₀ ∪ Σ₂. Satz über sternfreie Baumsprachen und anti-chain Logik, Anwendung für Alphabete der Form Σ=Σ₀ ∪ Σ₂;

    Material:

    • Folien 181-189
    • Skript 141-151

13. Di, 10.06.2025:
    • 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.
      Neues Kapitel 4: Abschnitt 1: unendliche Wörter und Sprachen: Def. ω-reguläre Sprachen, Abschluss unter Vereinigung und Linkskonkatenation

    Material:

    • Folien 189-209
    • Skript 151-166

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

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

14. Fr., 13.06.2025:
    • 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, 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

    Material:

    • Folien 209-222
    • Skript 166-178

15. Di., 17.06.2025:
    • 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), Safra-Konstruktion: Beispiel, McNaughton's Theorem, Beweis der Vollständigkeit der Konstruktion

    Material:

    • Folien 223-231
    • Skript 178-190

16. Fr., 20.06.2025:
    • McNaughton's Theorem, Beweis der Korrektheit der Konstruktion. Komplementierung Büchi-Automat. Leerheitsproblem, Äquivalenzproblem & Univeralitätsproblem für ndet. Büchi-Automaten.
      Alternierende Automaten, Def. & (gedächtnislose) Läufe

    Material:

    • Folien 233-240
    • Skript 190-197

17. Di., 24.06.2025:
    • Alternierende Automaten: Bew: Existenz gedächtnisloser Läufe bei Akzeptanz, Gleichmächtigkeit zu NBA

    Material:

    • Folien 237-244
    • Skript 195-201

18. Fr., 25.06.2025:
    • Alternierende Automaten und Komplementierung: AcoBA, ABA -> Komplement AcoBA, AcoBA -> ABA und insgesamt: Komplementierung NBA
      Alternierende Automaten und LTL: schleifenfreie ABA, LTL: positive Normalform, LTL <-> schleifenfreie ABA

    Material:

    • Folien 244-252
    • Skript 201-210

19. Fr., 04.07.2025:
    • Kapitel 5: unendliche Bäume, nichtdeterministische Baum-Automaten mit Büchi-, Müller- und Paritätsakzeptanzbedingung, Büchi vs. Müller
      Paritätsbaumautomaten vs. Müllerbaumautotan, dafür: LAR-Konstruktion;

    Material:

    • Folien 253-263
    • Skript 211-221