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{Jansen:479827,
      author       = {Jansen, Nils},
      othercontributors = {Ábrahám, Erika and Becker, Bernd and Katoen,
                          Joost-Pieter},
      title        = {{C}ounterexamples in probabilistic verification},
      school       = {Aachen, Techn. Hochsch.},
      type         = {Dissertation},
      address      = {Aachen},
      publisher    = {Publikationsserver der RWTH Aachen University},
      reportid     = {RWTH-2015-03318},
      pages        = {XI, 224 S.S. . graph. Darst.},
      year         = {2015},
      note         = {Aachen, Techn. Hochsch., Diss., 2015},
      abstract     = {The topic of this thesis is roughly to be classified into
                      the formal verification of probabilistic systems. In
                      particular, the generation of counterexamples for
                      discrete-time Markov Models is investigated. A
                      counterexample for discrete-time Markov Chains (DTMCs) is
                      classically defined as a (finite) set of paths. In this
                      work, this set of paths is represented symbolically as a
                      critical part of the original system, a so-called critical
                      subsystem. This notion is extended to Markov decision
                      processes (MDPs) and probabilistic automata (PAs). The
                      results are introduced in four parts: 1. A model checking
                      algorithm for DTMCs based on a decomposition of the system's
                      graph in strongly connected components (SCCs). This approach
                      is extended to parametric discrete-time Markov Chains. 2.
                      The generation of counterexamples for DTMCs and reachability
                      properties based on graph algorithms. A hierarchical
                      abstraction scheme to compute abstract counterexamples is
                      presented, followed by a general framework for both
                      explicitly represented systems and symbolically represented
                      systems using binary decision diagrams (BDDs). 3. The
                      computation of minimal critical subsystems using SAT modulo
                      theories (SMT) solving and mixed integer linear programming
                      (MILP). This is investigated for reachability properties and
                      $\omega$-regular properties on DTMCs, MDPs, and PAs. 4. A
                      new concept of high-level counterexamples for PAs. Markov
                      models can be specified by means of a probabilistic
                      programming language. An approach for computing critical
                      parts of such a symbolic description of a system is
                      presented, yielding human-readable counterexamples. All
                      results have been published in conference proceedings or
                      journals. A thorough evaluation on common benchmarks is
                      given comparing all methods and also competing with
                      available implementations of other approaches.},
      cin          = {121310 / 120000 / 123420},
      ddc          = {004},
      cid          = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$ /
                      $I:(DE-82)123420_20140620$},
      typ          = {PUB:(DE-HGF)11},
      urn          = {urn:nbn:de:hbz:82-rwth-2015-033184},
      url          = {https://publications.rwth-aachen.de/record/479827},
}