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{Horn:51451,
      author       = {Horn, Florian},
      othercontributors = {Thomas, Wolfgang},
      title        = {{R}andom games},
      address      = {Aachen},
      publisher    = {Publikationsserver der RWTH Aachen University},
      reportid     = {RWTH-CONV-113742},
      pages        = {137 S. : graph. Darst.},
      year         = {2008},
      note         = {Aachen, Techn. Hochsch., Diss., 2008},
      abstract     = {Games are a classical tool for the synthesis of controllers
                      in reactive systems. In this setting, a game is defined by:
                      an arena, which is a graph modelling the system and its
                      evolution; and a winning condition, which models the
                      specification that the controller must ensure. In each
                      state, the outgoing transition is chosen either by the
                      controller (Eve), an hostile environment (Adam), or a
                      stochastic law (Random). This process is repeated for an
                      infinite number of times, generating an infinite play whose
                      winner depends on the winning condition. Our first object of
                      study is the fundamental case of reachability games. We
                      present a new effective approach to the computation of the
                      values, based on permutations of random states. In terms of
                      complexity, the resulting "permutation algorithm" is
                      orthogonal to the classical, strategy-based algorithms: it
                      is exponential in the number of random states, but not in
                      the number of controlled states. We also present an
                      improvement heuristic for this algorithm, inspired by the
                      "strategy improvement" algorithm. We turn next to the very
                      general class of prefix-independent games. We prove the
                      existence of optimal strategies in these games. We also show
                      that our permutation algorithm can be extended into a
                      "meta-algorithm", turning any qualitative algorithm into a
                      quantitative algorithm. We study then the complexity of
                      optimal strategies for Muller games, focusing on the amount
                      of memory that can be saved through the use of randomised
                      strategies. Using the Zielonka tree, we show tight bounds on
                      the necessary and sufficient memory needed to define
                      randomised optimal strategies for any given Muller
                      condition. We also propose a polynomial algorithm for the
                      winner problem in explicit Muller games. The results of the
                      former chapter yield immediately NP and co-NP algorithms for
                      the values problem. Lastly, we consider the finitary
                      versions of parity and Streett games, where the regular
                      conditions are supplemented by universal bounds on delays.
                      We propose a polynomial algorithm for the winner problem on
                      finitary parity games. For finitary Streett games, a
                      reduction to Request-Response games provides an EXPTIME
                      algorithm for qualitative problems, and we show that the
                      problem is PSPACE-hard.},
      keywords     = {Verifikation (SWD) / Logiksynthese (SWD) / Kombinatorisches
                      Spiel (SWD) / Stochastisches Spiel (SWD) / Randomisierung
                      (SWD)},
      cin          = {120000 / 122110},
      ddc          = {004},
      cid          = {$I:(DE-82)120000_20140620$ / $I:(DE-82)122110_20140620$},
      shelfmark    = {G.3 * G.2.2 * D.2.4},
      typ          = {PUB:(DE-HGF)11},
      urn          = {urn:nbn:de:hbz:82-opus-29712},
      url          = {https://publications.rwth-aachen.de/record/51451},
}