Modelchecking auf Halbordnungsbasis

Auf dieser Seite

• Termine
• Inhalt
• Literatur

Termine

Modelchecking auf Halbordnungsbasis
(2. TEIL EINER STAMMVORLESUNG)

Form: 2 Stunden Vorlesung pro Woche; mündliche Prüfung (Fachgespräch).

Vorlesung: Dienstag 8:00 - 10:00 A10 Hörsaal F.

Erste Vorlesung: Dienstag, 16.10.2001.

Credits: 3.

Diese Vorlesung kann separat als Spezialvorlesung gehört werden. Sie ergänzt inhaltlich das Modul "Petrinetze" (6 Credits) des Sommersemesters 2001. Hörer/innen beider Vorlesungen können einen Stammvorlesungsschein (6 SWS) erwerben.

Inhalt

Unter Modelchecking versteht man den algorithmischen Nachweis von Systemeigenschaften bei unparametrisierten Systemen. (Beispiel: der Nachweis, dass ein Protokoll zum wechselseitigen Ausschluss diesen wirklich garantiert.) Je nachdem, welche Form der Systembeschreibung gewählt ist, können verschiedene Algorithmen unterschieden werden. In dieser Vorlesung konzentrieren wir uns auf Systeme, deren Zustandsmengen nicht direkt als beschriftete Graphen, sondern indirekt durch die (halbgeordnete) Menge ihrer Abläufe gegeben sind. Diese indirekte Darstellung bietet algorithmische Vor- und Nachteile. Die Vorlesung besteht im Wesentlichen aus der Darstellung verschiedener neuer Algorithmen aus der Fachliteratur (Konferenz- und Zeitschriftenpapiere). Es werden auch implementierte Systeme vorgestellt.

Literatur

Eine Auswahl aus den Arbeiten von Javier Esparza, Keijo Heljanko und Viktor Khomenko u.a. Es gibt über dieses neue Gebiet (noch) kein Lehrbuch. In der Vorlesung wird ein handschriftliches Skriptum ausgeteilt werden.