Verifikation unendlicher Systeme
-
Vortragender
-
Dr. Stefan Göller
-
Art der Veranstaltung
-
ECTS 6, Wahlbereich: Master-Ergänzung
-
Zeit und Ort
-
Mo 14–16, MZH 1470 (ab 14. 10.)
Di 14–16, MZH 4194 (Übung 14-tägig)
Lageplan Uni Bremen
Kurzbeschreibung
Die Analyse unendlicher Systeme ist vor allem bei der Modellierung und
Verifikation von Softwaresystemen von großer Bedeutung.
Die Unendlichkeit solcher Systeme ist beispielsweise
durch
-
die Verwendung von Variablen über einem unendlichen
Wertebereich,
-
der Synchronisierung unbeschränkt vieler Prozesse, oder
-
der unbeschränkten Rekursionstiefe
begründet.
Unendliche Transitionssysteme bieten sich besonders gut an, um
das Verhalten solcher Systeme auf eine abstrakte aber immer noch
hinreichend ausdrucksvolle Weise zu beschreiben.
Diese Vorlesung führt verschiedene Formalismen zur Beschreibung
unendlicher Transitionssysteme ein (wie z.B. Pushdownsysteme, Petrinetze,
automatische Graphen).
Ein Ziel der Vorlesung wird die Ausdrucksstärke dieser Systeme
bezüglich
Bisimulationsäquivalenz sein.
Desweiteren wird besonderes Augenmerk darauf gelegt werden welche Eigenschaften
dieser Systeme entscheidbar bleiben.
Solche Systemeigenschaften werden dabei in geeigneten Logiken,
insbesondere temporalen Logiken
(modaler μ-Kalkül, LTL, CTL), formalisiert.
Vorläufige Themenliste:
-
Erreichbarkeit und LTL Model Checking in Pushdownsystemen
-
Paritätsspiele auf Pushdownsystemen
-
Lossy-Channel Systeme
-
Überdeckungs- und Endlichkeitsprobleme für Petrinetze
-
Strikte Inklusion Mayr's PRS Hierarchie
Wissen aus der Veranstaltung "Theoretische Informatik 1" ist hilfreich,
wird aber nicht vorausgesetzt.
Übungsblätter
AG Theorie der künstlichen Intelligenz
1. 7. 2013
Stefan Göller
