Logik in der Informatik
Prof. Dr. Martin Grohe

Logbuch zur Vorlesung Logik, Spiele und Automaten

Di, 19.10.10: Skript S.1-8. Model-Checking; Beispiel: MUX; Transitionssysteme; Berechnungspfade
Do, 21.10.10: Skript S.9-13. Sprache eines Transitionssystems; Bisimilarität; Baumabwicklungen
Di, 26.10.10: Skript S.15-21. Arenen; Spiele; Partien; Strategien; Spielbam und Strategiebaum; Bisimulationsspiel
Do, 28.10.10: Skript S.21-24. Einfache Spiele; induktive Charakterisierung der Gewinnmengen; positionale Determiniertheit
Di, 2.11.10: Skript S.24-31. Linearzeitalgorithmus zum Lösen einfacher Spiele; Syntax und Sematik der Modallogik; Negationsnormalform
Do, 4.11.10: Skript S.32-36. Auswertungsspiel für die Modallogik; Bisimulationsinvarianz der Modallogik; n-Bisimulationen
Di, 9.11.10: Skript S.37-40. ML-Äquivalenz und n-Bisimulationen; Satz von Hennessy und Milner; Endliche-Modell-Eigenschaft
Do, 11.11.10: Skript S.41-49. Beweis der Endlichen-Modell-Eigenschaft (zu Ende); Entscheidbarkeit der Modallogik; Modallogik und Logik erster Stufe; Lineare Temporale Logik LTL
Di, 16.11.10: Skript S.50-53. Normalformen für LTL; LTL-Äquivalenz und Sprachäquivalenz von Transitionssystemen
Do, 18.11.10: Skript S.53-60. Baumzeitlogiken CTL* und CTL; Normalformen; Linearzeitalgorithmus für CTL-Model-Checking
Di, 23.11.10: Skript S.60-66. CTL-Model-Checking; Büchiautomaten; ω-reguläre Ausdrücke; Büchi-Automaten und Transitionssysteme; Automatenbasiertes Model-Checking
Do, 25.11.10: Skript S.66-72. Abschlusseigenschaften von Büchi-erkennbaren Sprachen (Durchschnitt, Vereinigung); Kombination mit regulären Sprachen
Di, 30.11.10: Skript S.73-77. Deterministische Büchi-Automaten; Komplementierung
Do, 2.12.10: Skript S.78-80. Komplementierung zu Ende
Di, 7.12.10: Skript S.80-85. Muller-Automaten; verallgemeinerte Büchi-Automaten; LTL auf Wörtern
Do, 9.12.10: Skript S.85-87. LTL und Büchi-Automaten
Di, 14.12.10: Skript S.88-89, Appendix B S.3-5. Autmatenbasierte Erfüllbarkeits- und Model-Checking-Algorithmen für LTL; Ordinalzahlen
Do, 16.12.10: Appendix B S.5-8. Ordinalzahlen und transfinite Induktion
Di, 4.1.11: Skript S.93-97 . Fixpunkte monotoner Operatoren; Satz von Knaster und Tarski; Dualitätssatz; induktive Definition des größten und kleinsten Fixpunkts
Do, 6.1.11: Skript S.97-99. Beispiele von Fixpunkten monotoner Operatoren
Di, 11.1.11: Skript S.99-103. Positive und negative Vorkommen von Symbolen in modallogischen Formeln; Syntax und Semantik des modalen μ-Kalküls
Do, 13.1.11: Skript S.104-108. Diskussion der Semantik des μ-Kalküls; Beispiele; Einbettung von CTL* in L_μ
Di, 18.1.11: Skript S.108-114. Infinitäre Modallogik; Abwicklungen von Formeln; Bisimulationsinvarianz von L_μ; Paritätsspiele
Do, 20.1.11: Skript S.114-117. Attraktoren und Fallen; positionale Strategien
Do, 27.1.11: Skript S.117-122. Positionale Determiniertheit; rekursiver Algorithmus zum Lösen von Paritätsspielen
Do, 3.2.11: Skript S.122-126. Lösen von Paritätsspielen in NP∩co-NP; Arena des Auswertungsspiels für den μ-Kalkül; Auswertungsspiel für Formeln mit einem Fixpunktoperator
Di, 8.2.11: Skript S.126-129. Auswertungsspiel für Formeln mit einem Fixpunktoperator; Rangfunktion für das Auswertungsspiel; Abwicklung von Paritätsspielen
Do, 10.2.11: Skript S.129-131. Beweis des Abwicklungslemmas
Di, 15.2.11: Vortrag Oliver Friedmann über Strategieverbesserungsalgorithmen (Folien hier
Do, 17.2.11: Skript S.131-132. Beweis der Adäquatheit des Auswertungsspiels.

Last modified: Mon Feb 28 12:36:02 CET 2011
Martin Grohe