h1

000974903 001__ 974903
000974903 005__ 20251106105845.0
000974903 0247_ $$2HBZ$$aHT030626337
000974903 0247_ $$2Laufende Nummer$$a42860
000974903 0247_ $$2datacite_doi$$a10.18154/RWTH-2023-11664
000974903 037__ $$aRWTH-2023-11664
000974903 041__ $$aEnglish
000974903 082__ $$a004
000974903 1001_ $$0P:(DE-82)IDM03493$$aSpel, Jip Josephine$$b0$$urwth
000974903 245__ $$aMonotonicity in Markov models$$cvorgelegt von Jip Spel, M.Sc.$$honline
000974903 260__ $$aAachen$$bRWTH Aachen University$$c2023
000974903 260__ $$c2024
000974903 300__ $$a1 Online-Ressource : Illustrationen
000974903 3367_ $$02$$2EndNote$$aThesis
000974903 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000974903 3367_ $$2BibTeX$$aPHDTHESIS
000974903 3367_ $$2DRIVER$$adoctoralThesis
000974903 3367_ $$2DataCite$$aOutput Types/Dissertation
000974903 3367_ $$2ORCID$$aDISSERTATION
000974903 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University 2024
000974903 502__ $$aDissertation, RWTH Aachen University, 2023$$bDissertation$$cRWTH Aachen University$$d2023$$gFak01$$o2023-07-07
000974903 5203_ $$aIn vielen Systemen treten Formen von Wahrscheinlichkeiten auf, unter anderem in Kommunikationsprotokollen, Zufallsprotokollen und biologischen Systemen vor. Solche Systeme können wir als Markow-Modelle modellieren, und anhand einer Spezifikation in (einer probabilistischen Erweiterung der) lineare temporalen Logik (LTL) oder baumbasierten temporalen Logik (CTL) verifizieren. Das Ziel ist die Berechnung der Wahrscheinlichkeit oder der erwarteten Gesamtkosten für das Erreichen eines der Teilzuständen. Die Wahrscheinlichkeiten in einem Markow-Modell werden oft als ein exakter Wert angegeben. In der Praxis sind diese Wahrscheinlichkeiten jedoch nicht genau bekannt, sondern liegen in einem Intervall. Außerdem können diese Wahrscheinlichkeiten von anderen Wahrscheinlichkeiten abhängen. Deshalb konzentrieren wir uns auf parametrische Markow-Modelle, in denen die Wahrscheinlichkeiten symbolisch durch Parameter in rationalen Funktionen dargestellt werden. In dieser Arbeit konzentrieren wir uns auf parametrische Markow-Ketten (pMCs) und parametrische Markow-Entscheidungsprozesse (pMDPs). Beide Arten von Markow-Modellen haben eine endliche Menge von Zuständen, von denen einer den Ausgangszustand darstellt, und einer oder mehrere Zielzustände sind. Die Übergänge zwischen den Zuständen werden mit einer parametrischen Wahrscheinlichkeitsfunktion gekennzeichnet. Bei pMCs ist diese Funktion für alle Zustände deterministisch; bei pMDPs kann diese Funktion auch für einige Zustände nicht-deterministisch sein. Eines der Probleme, das wir in dieser Arbeit analysieren, ist das sogenannte$$lger
000974903 520__ $$aMany systems exhibit probabilistic behavior, such as randomized protocols, communication protocols, or biological systems. Probabilistic model checking is a common way to analyze these type of systems. We often model these systems as Markov models and check them against a specification typically given in a probabilistic extension of LTL or CTL. One of the main goals is to analyze the probability to reach or the expected total reward upon reaching a set of target states. When checking for these properties, we assume probabilities to be fixed constants. In practice, however, these probabilities are often not fixed but bounded to a given interval. Moreover, these probabilities can be dependent on other probabilities. Therefore, we consider parametric Markov models, in which the probabilities are given symbolically by rational functions over parameters. We focus on parametric Markov chains (pMCs) and parametric Markov decision processes (pMDPs). Both models have a finite set of states, of which one is the initial state, and one or more are the target states. The transitions are given by a parametric transition function. PMCs have a deterministic transition function, whereas for pMDPs the transition function might be non-deterministic. One problem addressed when analyzing parametric Markov models is the almost- optimal synthesis problem, i.e., finding a parameter instantiation such that the expected total reward is$$leng
000974903 588__ $$aDataset connected to Lobid/HBZ
000974903 591__ $$aGermany
000974903 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor$$urwth
000974903 7001_ $$aPetrov, Tatjana$$b2$$eThesis advisor
000974903 8564_ $$uhttps://publications.rwth-aachen.de/record/974903/files/974903.pdf$$yOpenAccess
000974903 8564_ $$uhttps://publications.rwth-aachen.de/record/974903/files/974903_source.zip$$yRestricted
000974903 909CO $$ooai:publications.rwth-aachen.de:974903$$popenaire$$popen_access$$pVDB$$pdriver$$pdnbdelivery
000974903 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM03493$$aRWTH Aachen$$b0$$kRWTH
000974903 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00048$$aRWTH Aachen$$b1$$kRWTH
000974903 9141_ $$y2023
000974903 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000974903 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation)$$x0
000974903 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
000974903 9201_ $$0I:(DE-82)080060_20170720$$k080060$$lGraduiertenkolleg UnRAVeL$$x2
000974903 961__ $$c2024-01-29T11:57:48.210496$$x2023-12-12T11:37:54.080927$$z2024-01-29T11:57:48.210496
000974903 9801_ $$aFullTexts
000974903 980__ $$aI:(DE-82)080060_20170720
000974903 980__ $$aI:(DE-82)120000_20140620
000974903 980__ $$aI:(DE-82)121310_20140620
000974903 980__ $$aUNRESTRICTED
000974903 980__ $$aVDB
000974903 980__ $$aphd