Fr. 18.11.2011, Informatik-Kolloquium
Quantitative Analyse randomisierter Systeme und probabilistische Automaten, Prof. Dr. Christel Baier (TU Dresden) Zeit: 14:00 Uhr, c.t. Raum: Raum H-A 8107 (Hölderlinstraße)
Informatik-Kolloquium
Quantitative Analyse randomisierter Systeme
und probabilistische Automaten
Freitag, den 18.11.2011,
14:00 Uhr, c.t. , Raum H-A 8107 (Hölderlinstraße)
Referent: Prof. Dr. Christel Baier (TU Dresden)
Abstract: Probabilistische Phänomene treten in natürlicher Weise bei der Modellierung von Computersystemen
auf, z.B. in Form von Ausfallwahrscheinlichkeiten für Hardwarekomponenten, stochastischen Annahmen
über die Ausführungszeiten von Jobs, oder Protokollen, die mit Zufallszahlen operieren. Zur Verifikation
und quantitativen Analyse probabilistischer System wurden zahlreichen Methoden entwickelt. Der Vor-
trag befasst sich mit dem automaten-basierten Ansatz für Systeme, die durch einen Markovschen Ent-
scheidungsprozess modelliert werden können. Die Grundidee besteht darin, die gewünschte Systemei-
genschaft (z.B."kein Systemausfall" oder "jeder wartende Prozess erhält irgendwann die benötigte Re-
source") durch einen deterministischen Automaten darzustellen und mit Hilfe einer Produktkonstruktion
die Wahrscheinlichkeit für die gegebene Systemeigenschaft im schlimmsten Fall zu berechnen. Der Vor-
trag stellt diesen Ansatz kurz vor und erläutert dann die Idee der Partial Order Reduction, welche ver-
sucht Redundanzen, die sich aus der Kommutativität unabhängiger Aktionen ergeben, zu erkennen und
ein reduziertes Systemmodell zu erstellen. Weiter geht der Vortrag auf die Beobachtung ein, dass die
übliche Semantik von Markovschen Entscheidungsprozessen keinerlei Einschränkungen an die
Auflösung des Nichtdeterminismus im Systemmodell macht und daher zu unrealistischen Analyseergeb-
nissen führen kann. Das Modell von partiell-observierbaren Markovschen Entscheidungsprozessen be-
hebt zwar diese Anomalie, jedoch werden viele Verifikationsprobleme unentscheidbar, was auf die Ver-
wandtschaft von partiell-observierbaren Markovschen Entscheidungsprozessen und probabilistischen
Automaten als Sprachakzeptoren zurückzuführen ist..
.