Parameter synthesis in Markov models

Junges, Sebastian; Abate, Alessandro; Esparza, Javier; Katoen, Joost-Pieter

doi:10.18154/RWTH-2020-02348

Parameter synthesis in Markov models

Junges, Sebastian^RWTH*

2020

Verantwortlichkeitsangabevorgelegt von Sebastian Junges, M.Sc.

ImpressumAachen 2020

Umfang1 Online-Ressource (xv, 371 Seiten) : Illustrationen

Dissertation, RWTH Aachen University, 2020

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Abate, Alessandro (Thesis advisor) ; Esparza, Javier (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2020-02-13

Online
DOI: 10.18154/RWTH-2020-02348
URL: https://publications.rwth-aachen.de/record/783179/files/783179.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Markov chains (frei) ; Markov decision processes (frei) ; Markov models (frei) ; synthesis (frei) ; verification (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

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.

Markov models comprise states with probabilistic transitions. The analysis of these models is ubiquitous and studied in, among others, reliability engineering, artificial intelligence, systems biology, and formal methods. Naturally, their analysis crucially depends on the transition probabilities. Often, these probabilities are approximations based on data or reflect configurable parts of a modelled system. To represent the uncertainty about the probabilities, we study parametric Markov models, in which the probabilities are symbolic expressions rather than concrete values. More precisely, we consider parametric Markov decision processes (pMDPs) and parametric Markov chains (pMCs) as special case. Substitution of the parameters yields classical, parameter-free Markov decision processes (MDPs) and Markov chains (MCs).A pMDP thus induces uncountably many MDPs. Each MDP may satisfy reachability and reward properties, such as "the maximal probability that the system reaches an `offline' state is less than 0.01%", or "the maximal expected energy consumption is less than 20 kWh. "Lifting these properties to pMDPs yields fundamental problems asking: - "Is there an induced MDP satisfying the property?" (feasibility), its dual - "Do all induced MDPs satisfy the property?" (validity), and advanced problems such as "What is a concise representation for all induced MCs satisfying the property?" We study these problems on a conceptual level, and design and implement both improved and novel algorithms. On the conceptual side, a thorough discussion of the feasibility problem yields new results, such as: (1) that answering various variants of the feasibility problem is — in terms of complexity — as hard as finding roots of a multivariate polynomial, and (2) that these problems are tightly connected to the analysis of memoryless strategies in partially observable MDPs, a famous model in artificial intelligence. Additionally, we introduce family MCs (fMCs), a subclass of pMCs with finitely many induced MCs. Among others, fMCs define fundamental problems underlying the quantitative analysis of software product lines and sketching of probabilistic programs. On the algorithmic side, (1) we present and analyse improved but previously known approaches, and combine them to meet practical needs. Their analysis inspired (2) three new and orthogonal approaches, utilising advances in convex optimisation, as well as adapting prominent ideas such as inductive synthesis and abstraction-refinement to the particular setting. All methods efficiently exploit advances in the off-the-shelf analysis of MDPs. On the empirical side, the new methods improve the state-of-the-art considerably, handling hundreds of parameters and millions of states. All the approaches we present have been implemented in open-source tools.

OpenAccess:
PDF
(additional files)