h1

% IMPORTANT: The following is UTF-8 encoded.  This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.

@PHDTHESIS{Spel:974903,
      author       = {Spel, Jip Josephine},
      othercontributors = {Katoen, Joost-Pieter and Petrov, Tatjana},
      title        = {{M}onotonicity in {M}arkov models},
      school       = {RWTH Aachen University},
      type         = {Dissertation},
      address      = {Aachen},
      publisher    = {RWTH Aachen University},
      reportid     = {RWTH-2023-11664},
      pages        = {1 Online-Ressource : Illustrationen},
      year         = {2023},
      note         = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
                      University 2024; Dissertation, RWTH Aachen University, 2023},
      abstract     = {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},
      cin          = {121310 / 120000 / 080060},
      ddc          = {004},
      cid          = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$ /
                      $I:(DE-82)080060_20170720$},
      typ          = {PUB:(DE-HGF)11},
      doi          = {10.18154/RWTH-2023-11664},
      url          = {https://publications.rwth-aachen.de/record/974903},
}