h1

TY  - THES
AU  - Junges, Sebastian
TI  - Parameter synthesis in Markov models
PB  - RWTH Aachen University
VL  - Dissertation
CY  - Aachen
M1  - RWTH-2020-02348
SP  - 1 Online-Ressource (xv, 371 Seiten) : Illustrationen
PY  - 2020
N1  - Veröffentlicht auf dem Publikationsserver der RWTH Aachen University
N1  - Dissertation, RWTH Aachen University, 2020
AB  - 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
LB  - PUB:(DE-HGF)11
DO  - DOI:10.18154/RWTH-2020-02348
UR  - https://publications.rwth-aachen.de/record/783179
ER  -