Parameter synthesis in Markov models

Junges, Sebastian; Katoen, Joost-Pieter (Thesis advisor); Abate, Alessandro (Thesis advisor); Esparza, Javier (Thesis advisor)

Aachen (2020)
Doktorarbeit

Dissertation, RWTH Aachen University, 2020

Kurzfassung

Markow-Modelle umfassen Zustände mit wahrscheinlichkeitsbehafteten Transitionen. Die Analyse dieser Modelle ist allgegenwärtig. Sie ist Forschungsgegenstand, u.a. in der Zuverlässigkeitstechnik, der künstlichen Intelligenz, der Systembiologie und in den formalen Methoden. Die Analyse ist naturgemäß stark abhängig von den Transitionswahrscheinlichkeiten. Diese basieren oft auf Schätzungen oder spiegeln konfigurierbare Komponenten eines Systems wider. Um diesen Ungenauigkeiten gerecht zu werden, betrachten wir parametrische Markow-Modelle, in denen Wahrscheinlichkeiten durch symbolische Ausdrücke statt durch konkrete Werte dargestellt werden. Insbesondere betrachten wir parametrische Markow-Entscheidungsprozesse (pMDPs), sowie parametrische Markow-Ketten (pMCs) als einen Spezialfall. Das Ersetzen der Parameter induziert die klassischen parameterfreien Markow-Entscheidungs-prozesse (MDPs) und Markow-Ketten (MCs). Ein pMDP beschreibt demnach überabzählbar viele MDPs. Jeder MDP kann Erreichbarkeits- und Rewardeigenschaften erfüllen, beispielsweise - Die maximale Wahrscheinlichkeit, dass das System offline geht, beträgt weniger als 0,01% oder -der maximal erwartete Energieverbrauch ist geringer als 20 kWh. Für solche Eigenschaften und parametrischen Modelle ergeben sich dann folgende fundamentale Fragen:- Gibt es einen induzierten MDP, der die Eigenschaft erfüllt? (Feasibility) beziehungsweise das Duale: -Erfüllen alle induzierten MDPs die Eigenschaft? (Validity), sowie weiterführende Fragen, zum Beispiel: Gibt es eine kompakte Darstellung aller induzierten MCs, die eine Eigenschaft erfüllen? Wir untersuchen diese Fragestellungen konzeptuell, und entwerfen und implementieren sowohl verbesserte als auch neue Algorithmen. Auf der konzeptuellen Seite bietet eine ausführliche Diskussion neue Ergebnisse, wie zum Beispiel (1) das Beantworten von Varianten von Feasibility ist --- von der Komplexität her --- genau so schwer wie das Finden von Nullstellen eines multivariaten Polynoms und (2) diese Fragestellungen sind eng verwandt mit der Analyse von memoryless Strategien auf partially observable MDPs, einem elementaren Modell in der künstlichen Intelligenz. Außerdem führen wir Family MCs ein, eine Subklasse von pMCs mit endlich vielen induzierten MCs. Diese beschreiben wichtige Fragen aus der quantitativen Analyse von Software-Produktlinien, und dem Sketching von probabilistischen Programmen. Auf der algorithmischen Seite (1) präsentieren und analysieren wir verbesserte Ansätze sowie die Kombination solcher. Die Analyse inspiriert (2) drei neue Methoden, welche auf konvexer Optimierung und bedeutenden Ideen aus Inductive Synthesis und Abstraction-Refinement aufbauen. All diese Ansätze nutzen Neuerungen in der Analyse von MDPs aus. Die neuen Methoden verbessern den aktuellen Stand der Technik beträchtlich und sind in der Lage, Hunderte Parameter und Millionen Zustände zu verarbeiten. Alle vorgestellten Ansätze wurden implementiert in Open-Source Tools.

Einrichtungen

• Graduiertenkolleg UnRAVeL [080060]
• Fachgruppe Informatik [120000]
• Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) [121310]