h1

000783179 001__ 783179
000783179 005__ 20230408004327.0
000783179 0247_ $$2HBZ$$aHT020375883
000783179 0247_ $$2Laufende Nummer$$a38989
000783179 0247_ $$2datacite_doi$$a10.18154/RWTH-2020-02348
000783179 037__ $$aRWTH-2020-02348
000783179 041__ $$aEnglish
000783179 082__ $$a004
000783179 1001_ $$0P:(DE-82)IDM01624$$aJunges, Sebastian$$b0$$urwth
000783179 245__ $$aParameter synthesis in Markov models$$cvorgelegt von Sebastian Junges, M.Sc.$$honline
000783179 260__ $$aAachen$$c2020
000783179 300__ $$a1 Online-Ressource (xv, 371 Seiten) : Illustrationen
000783179 3367_ $$02$$2EndNote$$aThesis
000783179 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000783179 3367_ $$2BibTeX$$aPHDTHESIS
000783179 3367_ $$2DRIVER$$adoctoralThesis
000783179 3367_ $$2DataCite$$aOutput Types/Dissertation
000783179 3367_ $$2ORCID$$aDISSERTATION
000783179 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University
000783179 502__ $$aDissertation, RWTH Aachen University, 2020$$bDissertation$$cRWTH Aachen University$$d2020$$gFak01$$o2020-02-13
000783179 5203_ $$aMarkow-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.$$lger
000783179 520__ $$aMarkov 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.$$leng
000783179 588__ $$aDataset connected to Lobid/HBZ
000783179 591__ $$aGermany
000783179 653_7 $$aMarkov chains
000783179 653_7 $$aMarkov decision processes
000783179 653_7 $$aMarkov models
000783179 653_7 $$asynthesis
000783179 653_7 $$averification
000783179 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor$$urwth
000783179 7001_ $$0P:(DE-82)010759$$aAbate, Alessandro$$b2$$eThesis advisor
000783179 7001_ $$aEsparza, Javier$$b3$$eThesis advisor
000783179 8564_ $$uhttps://publications.rwth-aachen.de/record/783179/files/783179.pdf$$yOpenAccess
000783179 8564_ $$uhttps://publications.rwth-aachen.de/record/783179/files/783179_source.zip$$yRestricted
000783179 8564_ $$uhttps://publications.rwth-aachen.de/record/783179/files/783179.gif?subformat=icon$$xicon$$yOpenAccess
000783179 8564_ $$uhttps://publications.rwth-aachen.de/record/783179/files/783179.jpg?subformat=icon-1440$$xicon-1440$$yOpenAccess
000783179 8564_ $$uhttps://publications.rwth-aachen.de/record/783179/files/783179.jpg?subformat=icon-180$$xicon-180$$yOpenAccess
000783179 8564_ $$uhttps://publications.rwth-aachen.de/record/783179/files/783179.jpg?subformat=icon-640$$xicon-640$$yOpenAccess
000783179 8564_ $$uhttps://publications.rwth-aachen.de/record/783179/files/783179.jpg?subformat=icon-700$$xicon-700$$yOpenAccess
000783179 909CO $$ooai:publications.rwth-aachen.de:783179$$popenaire$$pVDB$$pdnbdelivery$$pdriver$$popen_access
000783179 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM01624$$aRWTH Aachen$$b0$$kRWTH
000783179 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00048$$aRWTH Aachen$$b1$$kRWTH
000783179 9141_ $$y2020
000783179 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000783179 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation)$$x0
000783179 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
000783179 9201_ $$0I:(DE-82)080060_20170720$$k080060$$lGraduiertenkolleg UnRAVeL$$x2
000783179 961__ $$c2020-03-03T14:53:51.813152$$x2020-02-19T09:32:34.449529$$z2020-03-03T14:53:51.813152
000783179 9801_ $$aFullTexts
000783179 980__ $$aI:(DE-82)080060_20170720
000783179 980__ $$aI:(DE-82)120000_20140620
000783179 980__ $$aI:(DE-82)121310_20140620
000783179 980__ $$aUNRESTRICTED
000783179 980__ $$aVDB
000783179 980__ $$aphd