|
Logik in der Informatik
PD Dr. Louchka Popova-Zeugmann |
|
Inhalt: Die Die meisten Methoden für die automatische Verifikation von nebenläufigen Systemen basieren auf der Betrachtung der gesamten Zustandsräume der Systeme. Das Problem dabei ist die so genannte "Zustandexplosion". In diesem Seminar werden wir die Entfaltungsmethode (unfolding method) betrachten, die eine Möglichkeit ist, die Zustandsexplosion zu mildern. Dabei werden wir einen Algorithmus für das Model Checking von nebenläufigen Systemen kennenlernen, der auf der Entfaltungsmethode basiert.
Vorträge: als pdf-File.
Termine: als pdf-File.
PD Dr.Louchka Popova-Zeugmann