h1

%0 Thesis
%A Spel, Jip Josephine
%T Monotonicity in Markov models
%I RWTH Aachen University
%V Dissertation
%C Aachen
%M RWTH-2023-11664
%P 1 Online-Ressource : Illustrationen
%D 2023
%Z Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2024
%Z Dissertation, RWTH Aachen University, 2023
%X 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
%F PUB:(DE-HGF)11
%9 Dissertation / PhD Thesis
%R 10.18154/RWTH-2023-11664
%U https://publications.rwth-aachen.de/record/974903