Quantitatives Model Checking WS 2020/21, Anne Remke, Carina Pilch, Stefan Schupp

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.

Kurs im HIS-LSF