Di, 13.4.04:
Einführung und Organisatorisches; Modellierung mit
Transitionssystemen (Definition und Beispiele). Folien.
Do, 15.4.04: Modellierung mit Transitionssystemen
(Beispiel, allgemeine Bemerkungen); Verifikation als
Model-Checking Problem, Synthese und Erfüllbarkeitsproblem;
Berechnungspfade und die Sprache eines Systems
Do, 29.4.04:
Determiniertheit und Existenz gedächtnisloser Gewinnstrategien
für einfache Spiele; Linearzeitalgorithmus zum Lösen einfacher
Spiele. Folie mit dem Algorithmus.
Do, 6.5.04:
FO-Model-Checking; Syntax und Semantik der Modallogik;
Model-Checking Spiel für die Modallogik.
Di, 11.5.04:
Model-Checking für die Modallogik; Modallogik und Bisimulation;
n-Bisimulation.
Übungsblatt 4.
Do, 13.5.04:
Satz von Hennessy und Milner; Endliche Modelleigenschaft der
Modallogik; Entscheidbarkeit des Erfüllbarkeitsproblems; Modal-Logik und Logik der 1. Stufe.
Di, 18.5.04:
Lineare Temporale Logik (LTL): Syntax und Semantik,
grundlegende Äquivalenzen und NNF, LTL-Äquivalenz vs Sprache
der Systeme.
Übungsblatt 5.
Di, 25.5.04:
Computation Tree Logic CTL* und CTL: Syntax und
Sematik, Vergleich der Logiken LTL, CTL* und CTL,
Model-Checking für CTL
Do, 27.5.04:
Büchi-Automaten: Einführung, Beschreibung von
Transitionssystemen mit Büchi-Automaten und Idee des
automatenbasierten Modelchecking, Abschluss unter Vereinigung
