Quantitatives Model Checking - Einzelansicht

Quantitatives Model Checking zielt darauf ab, Eigenschaften von randomisierten Modellen und Algorithmen zu verifizieren. Wir betrachten verschiedene Modellformalismen, von einfachen Transitionssystemen über Markov Ketten zu Markov Entscheidungsprozessen. Zu jeder Modellklasse wird die entsprechende Logik  vorgestellt, mit Hilfe derer auch komplexere Eigenschaften ausgedrückt werden können. Weiterhin werden zu jeder Logik die entsprechenden Algorithmen zum  Model Checking vorgestellt, die es ermöglichen, Eigenschaften zu verifizieren.

Neben dem Verständnis und der "händischen" Anwendung dieser Algorithmen sollen die erworbenen Kentnisse auch an Hand von Praxisbeispielen im Model Checking Tool PRISM eingesetzt werden. Hier können dann automatisiert größere und zum Teil parametrisierte Modelle verifiziert werden. Anwendungsbeispiele umfassen verschiedene randomisierte Algorithmen, sowie dynamisches Power Management.

Diese Vorlesung soll einen Überblick über Formalismen vermitteln, die verwendet werden können, wenn quantitative Aspekte, wie Zeit, Wahrscheinlichkeiten und Ressourcen eine zentrale Rolle spielen. Beim quantitativen Model Checking werden Wahrscheinlichkeiten für bestimmte Systemzustände errechnet, die dann mit bestehenden Wahrscheinlichkeitsschranken verglichen werden. Die Verfahren eignen sich daher besonders für die Bewertung der Zuverlässigkeit von - unter anderem - Eingebetteten Systemen.

Bei fehlenden Kombinationsmöglichkeiten für das QISPOS (Prüfungsnummern 11003, 11004 etc.) im MSc Informatik bzw. im Nebenfach Informatik im MSc Mathematik bitte an die Studienkoordination/Fachstudienberatung wenden!