% 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{Holtmann:64650,
author = {Holtmann, Michael},
othercontributors = {Thomas, Wolfgang},
title = {{M}emory and delay in regular infinite games},
address = {Aachen},
publisher = {Publikationsserver der RWTH Aachen University},
reportid = {RWTH-CONV-125929},
pages = {X, 147 S. : graph. Darst.},
year = {2011},
note = {Zsfassung in dt. und engl. Sprache; Aachen, Techn.
Hochsch., Diss., 2011},
abstract = {Infinite two-player games constitute a powerful and
flexible framework for the design and verification of
reactive systems. It is well-known that, for example, the
construction of a controller acting indefinitely within its
environment can be reduced to the computation of a winning
strategy in an infinite game (Pnueli and Rosner, 1989). For
the class of regular games, Büchi and Landweber (1969)
showed that one of the players has a winning strategy which
can be realized by a finite-state automaton. Based on this
fundamental result, many efforts have been made by the
research community to improve the solution methods for
infinite games. This is meant with respect to both the time
needed to compute winning strategies and the amount of space
required to implement them. In the present work we are
mainly concerned with the second aspect. We study two
problems related to the construction of small controller
programs. In the first part of the thesis, we address the
classical problem of computing finite-state winning
strategies which can be realized by automata with as little
memory, i.e., number of states, as possible. Even though it
follows from a result of Dziembowski et al. (1997) that
there exist exotic regular games for which the size of
automata implementing winning strategies is at least
exponential in the size of the game arena, most practical
cases require far less space. We propose an efficient
algorithm which reduces the memory used for the
implementation of winning strategies, for several classes of
regular conditions, and we show that our technique can
effect an exponential gain in the size of the memory. In the
second part of this thesis, we introduce a generalized
notion of a strategy. One of the players is allowed to delay
each of his moves for a finite number of steps, or, in other
words, exploit in his strategy some lookahead on the moves
of the opponent. This setting captures situations in
distributed systems, for example, when buffers are present
in communication between remote components. Our concept of
strategies corresponds to the class of continuous operators,
thereby extending the work of Hosch and Landweber (1972)
and, in particular, that of Büchi and Landweber (1969). We
show that the problem whether a given regular specification
is solvable by a continuous operator is decidable and that
each continuous solution can be reduced to one of bounded
lookahead. From our results, we derive a generalized
determinacy of regular conditions.},
keywords = {Unendliches Spiel (SWD) / Automatentheorie (SWD)},
cin = {122110 / 120000},
ddc = {004},
cid = {$I:(DE-82)122110_20140620$ / $I:(DE-82)120000_20140620$},
typ = {PUB:(DE-HGF)11},
urn = {urn:nbn:de:hbz:82-opus-37919},
url = {https://publications.rwth-aachen.de/record/64650},
}
guest ::