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