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{Hensel:752011,
      author       = {Hensel, Hans Christian},
      othercontributors = {Katoen, Joost-Pieter and Parker, David},
      title        = {{T}he probabilistic model checker {S}torm : symbolic
                      methods for probabilistic model checking},
      volume       = {2018-06},
      school       = {RWTH Aachen University},
      type         = {Dissertation},
      address      = {Aachen},
      publisher    = {RWTH Aachen University, Department of Computer Science},
      reportid     = {RWTH-2018-231803},
      series       = {Aachener Informatik-Berichte},
      pages        = {1 Online-Ressource (vii, 331 Seiten) : Illustrationen},
      year         = {2018},
      note         = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
                      2019; Dissertation, RWTH Aachen University, 2018},
      abstract     = {In a world in which we increasingly rely on safety critical
                      systems that simultaneously are becoming ever more complex,
                      formal methods provide a means to mathematically rigorously
                      prove systems correct. Model checking is a fully automated
                      technique that is successfully applied in the verification
                      of software and hardware circuits. However, in practice many
                      systems exhibit stochastic behavior, for instance when
                      components may fail or randomization is used as a key
                      element to improve efficiency. Probabilistic model checking
                      extends traditional (qualitative) model checking to deal
                      with such systems. As model checking can be (simplistically)
                      viewed as an exhaustive exploration of the state space of
                      the model under consideration, it suffers from the curse of
                      dimensionality: State spaces grow exponentially in the
                      number of components and variables and they quickly become
                      too large to be effectively manageable, a problem that is
                      typically referred to as state space explosion. Symbolic
                      methods have helped to alleviate this problem substantially.
                      Rather than considering states and transitions of the system
                      individually, they instead exploit structure in the model
                      and treat sets of states and transitions simultaneously.
                      Model checkers based on symbolic techniques dominate the
                      landscape of hardware and software model checking. In the
                      probabilistic setting, symbolic methods too show potential
                      but are arguably not on par with their qualitative
                      counterparts. This thesis is concerned with advances in the
                      field of symbolic techniques in the context of probabilistic
                      model checking. The major contributions are fivefold: (1) We
                      propose the JANI modeling language to unify the multitude of
                      input languages of probabilistic model checkers. It covers a
                      large range of models involving randomization and timing
                      aspects and offers well-defined points for future
                      extensions. (2) We show how counterexamples on the level of
                      JANI specifications can be synthesized. For this, we develop
                      a method based on the connection of standard probabilistic
                      model checking and a smart enumeration of the solutions of a
                      satisfiability problem. (3) We combine the strengths of
                      decision diagrams for the representation of gigantic systems
                      and bisimulation minimization, a technique that reduces
                      systems by factoring out symmetry. Our implementation is
                      shown to drastically reduce the sizes of models involving
                      probabilities, continuous time, nondeterminism and rewards.
                      (4) We summarize, extend and implement a game-based
                      abstraction-refinement framework that is able to treat
                      infinite-state probabilistic automata. In contrast to other
                      implementations, ours is openly available and computes
                      strictly sound bounds through the use of rational
                      arithmetic. (5) We present Storm, a new high-performance
                      probabilistic model checker. It goes beyond the standard
                      verification tasks through numerous features and in
                      particular integrates the items (1) to (4) above. We show
                      that it outperforms other state-of-the-art model checkers on
                      the majority of instances of the PRISM benchmark suite.},
      cin          = {121310 / 120000},
      ddc          = {004},
      cid          = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$},
      typ          = {PUB:(DE-HGF)11 / PUB:(DE-HGF)3},
      doi          = {10.18154/RWTH-2018-231803},
      url          = {https://publications.rwth-aachen.de/record/752011},
}