Universität Leipzig Institut für Informatik Automaten und Sprachen Karin Quaas | |||
Sommersemester 2015 Vorlesung Verifikation |
|||
Kursinhalte | |||
u.a. Model Checking, Temporale Logiken (LTL, CTL), Büchi-Automaten, Erreichbarkeitsproblem, Unendliche Transitionssysteme. | |||
Anforderungen | |||
Der Kurs läuft im Kernmodul (10-202-2107), Angewandte Automatentheorie. Vorkenntnisse in Diskreten Strukturen, Logik, Automaten und Sprachen sowie Komplexitätstheorie sind von Nutzen. | |||
Termine | |||
Vorlesung: Montags 13:15-14:45, P 801. | |||
Übungen: Freitags 11:15-11:45, P 410, aller zwei Wochen, ab 15.5. | |||
Die nächste Übung findet am Freitag dem 10.7. statt. | |||
Die Klausur fand am Montag, 13.7.2015, 13:15-14:45, im Raum P702 statt. Die Ergebnisse habe ich Ihnen am Abend 13.7.2015 per Email mitgeteilt. Falls eine Klausureinsicht gewüscht ist, so machen Sie bitte bis Donnerstag 16.7. einen Termin mit mir aus. | |||
Kursmaterial | |||
Mutual Exclusion Beispiel | |||
LTL | |||
Teil des Äquivalenzbeweises Übung 4 | |||
1. Aufgabenblatt, zur Besprechung am 15.5. | |||
Büchi-Automat Produktkonstruktion | |||
Nachtrag zur Übung am 15.5. | |||
Von LTL zu Generalisierten Büchi-Automaten | |||
2. Aufgabenblatt , zur Besprechung am 29.5. | |||
Teil des Korrektheitsbeweises LTL--Büchi-Automat | |||
3. Aufgabenblatt , zur Abgabe am 22.6., Besprechung am 26.6. | |||
4. Aufgabenblatt , Besprechung am 10.7. | |||
Literatur | |||
Specification and Verification using Temporal Logics, (S. Demri und P. Gastin), in: Modern Applications of Automata Theory, S. 457-494, 2012. | |||
Christel Baier und Joost-Pieter Katoen: Principles of Model Checking. Online-Version |