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{Schupp:767529,
      author       = {Schupp, Stefan},
      othercontributors = {Ábrahám, Erika and Frehse, Goran},
      title        = {{S}tate set representations and their usage in the
                      reachability analysis of hybrid systems},
      school       = {RWTH Aachen University},
      type         = {Dissertation},
      address      = {Aachen},
      reportid     = {RWTH-2019-08875},
      pages        = {1 Online-Ressource (217 Seiten) : Illustrationen,
                      Diagramme},
      year         = {2019},
      note         = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
                      University; Dissertation, RWTH Aachen University, 2019},
      abstract     = {Hybrid systems in computer science are systems with
                      combined discrete-continuous behavior. This work presents
                      results obtained in the field of safety verification for
                      linear hybrid systems whose continuous behavior can be
                      described by linear differential equations. We focus on a
                      special technique named flowpipe-construction-based
                      reachability analysis, which over-approximates the reachable
                      states of a given hybrid system as a finite union of state
                      sets. In these computations we can use different geometric
                      and symbolic representations for state sets as datatypes.
                      The choice of the state set representation has a strong
                      impact on the precision of the approximation and on the
                      running time of the analysis method. Additionally, numerous
                      further parameters and heuristics influence the analysis
                      outcome. In this work we investigate on the influence and
                      optimal usage of these parameters. Our results are collected
                      in a publicly available open-source C++ programming library
                      named HyPro. The major contributions of this work are
                      threefold: 1) We present our HyPro library offering
                      implementations for several state set representations that
                      are commonly used in flowpipe-construction-based
                      reachability analysis. A unified interface in combination
                      with reduction and conversion methods supports the fast
                      implementation of versatile analysis methods for linear
                      hybrid systems. 2) We put our library to practice and show
                      its applicability by embedding a flowpipe-construction-based
                      reachability analysis method in a CEGAR-based abstraction
                      refinement framework. The parallelization of this approach
                      further increases its performance. 3) We introduce methods
                      to decompose the search space and replace high-dimensional
                      computations by computations in lower-dimensional subspaces.
                      This method is applicable under certain conditions. An
                      automated check of these conditions, an automated
                      decomposition, and the integration of dedicated analysis
                      methods for subspace computations extend our approach.},
      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-2019-08875},
      url          = {https://publications.rwth-aachen.de/record/767529},
}