guest ::
| 001 | 974903 | ||
| 005 | 20251106105845.0 | ||
| 024 | 7 | _ | |2 HBZ |a HT030626337 |
| 024 | 7 | _ | |2 Laufende Nummer |a 42860 |
| 024 | 7 | _ | |2 datacite_doi |a 10.18154/RWTH-2023-11664 |
| 037 | _ | _ | |a RWTH-2023-11664 |
| 041 | _ | _ | |a English |
| 082 | _ | _ | |a 004 |
| 100 | 1 | _ | |0 P:(DE-82)IDM03493 |a Spel, Jip Josephine |b 0 |u rwth |
| 245 | _ | _ | |a Monotonicity in Markov models |c vorgelegt von Jip Spel, M.Sc. |h online |
| 260 | _ | _ | |a Aachen |b RWTH Aachen University |c 2023 |
| 260 | _ | _ | |c 2024 |
| 300 | _ | _ | |a 1 Online-Ressource : Illustrationen |
| 336 | 7 | _ | |0 2 |2 EndNote |a Thesis |
| 336 | 7 | _ | |0 PUB:(DE-HGF)11 |2 PUB:(DE-HGF) |a Dissertation / PhD Thesis |b phd |m phd |
| 336 | 7 | _ | |2 BibTeX |a PHDTHESIS |
| 336 | 7 | _ | |2 DRIVER |a doctoralThesis |
| 336 | 7 | _ | |2 DataCite |a Output Types/Dissertation |
| 336 | 7 | _ | |2 ORCID |a DISSERTATION |
| 500 | _ | _ | |a Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2024 |
| 502 | _ | _ | |a Dissertation, RWTH Aachen University, 2023 |b Dissertation |c RWTH Aachen University |d 2023 |g Fak01 |o 2023-07-07 |
| 520 | 3 | _ | |a In 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 |l ger |
| 520 | _ | _ | |a Many 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 |l eng |
| 588 | _ | _ | |a Dataset connected to Lobid/HBZ |
| 591 | _ | _ | |a Germany |
| 700 | 1 | _ | |0 P:(DE-82)IDM00048 |a Katoen, Joost-Pieter |b 1 |e Thesis advisor |u rwth |
| 700 | 1 | _ | |a Petrov, Tatjana |b 2 |e Thesis advisor |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/974903/files/974903.pdf |y OpenAccess |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/974903/files/974903_source.zip |y Restricted |
| 909 | C | O | |o oai:publications.rwth-aachen.de:974903 |p dnbdelivery |p driver |p VDB |p open_access |p openaire |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)IDM03493 |a RWTH Aachen |b 0 |k RWTH |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)IDM00048 |a RWTH Aachen |b 1 |k RWTH |
| 914 | 1 | _ | |y 2023 |
| 915 | _ | _ | |0 StatID:(DE-HGF)0510 |2 StatID |a OpenAccess |
| 920 | 1 | _ | |0 I:(DE-82)121310_20140620 |k 121310 |l Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) |x 0 |
| 920 | 1 | _ | |0 I:(DE-82)120000_20140620 |k 120000 |l Fachgruppe Informatik |x 1 |
| 920 | 1 | _ | |0 I:(DE-82)080060_20170720 |k 080060 |l Graduiertenkolleg UnRAVeL |x 2 |
| 980 | 1 | _ | |a FullTexts |
| 980 | _ | _ | |a I:(DE-82)080060_20170720 |
| 980 | _ | _ | |a I:(DE-82)120000_20140620 |
| 980 | _ | _ | |a I:(DE-82)121310_20140620 |
| 980 | _ | _ | |a UNRESTRICTED |
| 980 | _ | _ | |a VDB |
| 980 | _ | _ | |a phd |
| Library | Collection | CLSMajor | CLSMinor | Language | Author |
|---|