Logbuch zur Vorlesung Logik, Spiele und Automaten

Di, 15.4.08: Motiavtion: Model Checking, MUX-Protokoll; Transitionssysteme, Bisimulation, Sprachen, Baumabwicklungen, bis zum Ende von Kapitel 1.
Do, 17.4.08: Kapitel 2: Spiele, Gewinnstrategien, Bisimulationsspiel bis zur Definition von einfachen Spielen.
Di, 22.4.08: Einfache Spiele, Determiniertheit und Positionalität, Algorithmus für ES.
Do, 24.4.08: Kap. 3: Syntax und Semantik der Modallogik, Model-Checking in Linearzeit (mit Hilfe von Spielen).
Di, 29.4.08: Abschnitt 3.2: Modallogik und Bisimulation, Modaltiefe, n-Bisimulation, Satz von Hennessy und Milner
Di, 06.05.08 Abschnitt 3.3: Die Modallogik hat die endliche Modelleigenschaft, das Erfüllbarkeitsproblem der ML ist entscheidbar, Abschnitt 3.4: ML als Fragment der Logik erster Stufe
Do, 08.05.08 Kapitel 4: Temporale Logik. Abschnitt 4.1: Syntax und Semantik von LTL, LTL und Bisimulation, LTL-Äquivalenz und Sprachen von Transitionssystemen, Abschnitt 4.2: Syntax und Semantik von CTL und CTL*, Beispiele und Eigenschaften, ML als Fragment von CTL.
Di, 13.05.08 Kapitel 4 zuende: Model-Checking für CTL, Kapitel 5: Büchi-Automaten, Automatenbasiertes Model-Checking
Do, 15.05.08 Abschlusseigenschaften Büchi-erkennbarer Sprachen und Charakterisierung der Büchi-erkennbaren Sprachen
Di, 20.05.08 Charakterisierung der Büchi-erkennbaren Sprachen zuende, deterministische Büchi-Automaten, Komplementierung nicht-deterministischer Büchi-Automaten
Do, 22.05.08 Komplementierung nicht-deterministischer Büchi-Automaten zuende, Abschnitt über Muller-Automaten.
Di, 27.05.08 Kapitel 5.6: Büchi-Automaten und LTL: Übersetzung von LTL-Formeln in Büchi-Automaten, Leerheitstest für Büchi-Automaten, Erfüllbarkeits- und Auswertungsproblem von LTL.
Do, 29.05.08 Kapitel 5 zuende: Das LTL-Auswertungsproblem ist co-NP-schwer. Einschub: Ordinalzahlen und transfinite Induktion.
Di, 03.06.08 Einschub über Ordinalzahlen und transfinite Induktion zuende, Kapitel 6.1: Fixpunkte monotoner Funktionen, bis zum Satz von Knaster und Tarski.
Do, 05.06.08 Kapitel 6.1: Dualitätssatz, Fixpunkte und Induktionsstufen, Beispiele von Fixpunkten monotoner Funktionen.
Di, 10.06.08 Kapitel 6.2: Fixpunkte modallogischer Formeln, Syntax und Semantik des modalen μ-Kalküls,
Do, 12.06.08 Kapitel 6 zuende: Jede CTL-Formel ist äquivalent zu einer Formel des modalen μ-Kalküls, infinitäre Modallogik, die infinitäre Modallogik ist bisimulationsinvariant, der modale μ-Kalkül ist bisimulationsinvariant
Di, 17.06.08 Tag der Informatik
Do, 19.06.08 Kapitel 7: Definition von Paritätsspielen, Fallen, Attraktoren, Attraktorstrategien, bis Lemma 7.10.
Di, 24.06.08 Kapitel 7.1 zuende: Paritätsspiele sind positional determiniert, das Paritätsspielproblem liegt im Schnitt von NP und co-NP, Kapitel 7.2 bis zur Definition der Arena von Auswertungsspielen.
Do, 26.06.08 Spielcharakterisierungen für μ-Kalkül-Formeln mit höchstens einem Fixpunktoperator, bis zur Definition von Abwicklungen von Paritätsspielen.
Di, 01.07.08 Abwicklungslemma, Spielcharakterisierung für beliebige μ-Kalkül-Formeln.
Do, 03.07.08 Kapitel 7 zuende: Abhängigkeitsordnung, Alternationstiefe, verfeinerte Rangfunktion. Kapitel 8.1: Paritätsbaumautomaten, bis Definition 8.6.
Di, 08.07.08 Kapitel 8.1: Beispiele für Paritätsbaumautomaten. Abschlusseigenschaften von Paritätsbaumautomaten nur erwähnt, Entscheidbarkeit des Leerheitstests nur erwähnt. Weiter in Kapitel 8.5: Die Monadische Logik der zweiten Stufe (MSO), Syntax und Semantik, Beispiele. Satz MSO umfasst den μ-Kalkül nur erwähnt.
Do, 10.07.08 Entscheidbarkeit von S2S, Ausblick: Entscheidbarkeit des modalen μ-Kalküls.

Last modified: Thu July 10 15:14 CEST 2008
Isolde Adler