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{Quatmann:971553,
      author       = {Quatmann, Tim},
      othercontributors = {Katoen, Joost-Pieter and Randour, Mickael},
      title        = {{V}erification of multi-objective {M}arkov models},
      school       = {RWTH Aachen University},
      type         = {Dissertation},
      address      = {Aachen},
      publisher    = {RWTH Aachen University},
      reportid     = {RWTH-2023-09669},
      pages        = {1 Online-Ressource : Illustrationen},
      year         = {2023},
      note         = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
                      University; Dissertation, RWTH Aachen University, 2023},
      abstract     = {Probabilistic systems evolve based on environmental events
                      that occur with a certain probability. For such systems to
                      perform well, we are often interested in multiple
                      objectives, i.e., quantitative performance measures like the
                      probability of a failure or the expected time until task
                      completion. Sometimes, these objectives conflict with each
                      other: minimizing the failure probability possibly means
                      completing the task takes longer. Compromises need to be
                      found. We consider Markov models---particularly Markov
                      decision processes (MDPs) and Markov Automata (MAs). These
                      state-based modeling formalisms describe a system in its
                      random environment. Starting from an initial state, the
                      transitioning behavior in MDPs is determined by
                      probabilistic and nondeterministic choices. MAs further
                      extend MDPs by exponentially distributed continuous time
                      delays. Rewards can be attached to states or transitions to
                      model system quantities such as energy consumption,
                      productivity, or monetary costs. Objectives are formally
                      specified by a mapping from (infinite) system executions to
                      the value of interest, e.g., the total accumulated costs or
                      the average energy consumption. The expected value of an
                      objective is defined once the nondeterminism is resolved
                      using a strategy---intuitively reflecting the choices of a
                      system controller. Different strategies induce different
                      expected objective values. Multi-objective verification of
                      MDPs and MAs analyzes the interplay between the considered
                      objectives and identifies which trade-offs between expected
                      objective values are possible, i.e., achievable by some
                      strategy. We study practically efficient methods to compute
                      the set of achievable solutions. For this, we establish a
                      general framework and its instantiation for (undiscounted)
                      total reachability reward objectives, long-run average
                      reward objectives, and reward-bounded objectives. We
                      propagate the errors made by approximative methods, yielding
                      sound under- and over-approximations. We further consider
                      multi-dimensional quantiles that ask under which reward
                      constraints a given objective value is achievable. Finally,
                      we investigate a setting in which the strategies must be
                      simple, i.e., non-randomized and with limited memory access.
                      All presented approaches are integrated into the
                      state-of-the-art probabilistic model checker Storm. An
                      extensive evaluation of this implementation on a broad set
                      of multi-objective benchmarks shows that our approaches
                      scale to large models with millions of states.},
      cin          = {121310 / 120000},
      ddc          = {004},
      cid          = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$},
      typ          = {PUB:(DE-HGF)11},
      doi          = {10.18154/RWTH-2023-09669},
      url          = {https://publications.rwth-aachen.de/record/971553},
}