guest ::
TY - THES AU - Fridman, Wladimir TI - A study of pushdown games CY - Aachen PB - Publikationsserver der RWTH Aachen University M1 - RWTH-CONV-143589 SP - IX, 155 S. : graph. Darst. PY - 2013 N1 - Zsfassung in dt. und engl. Sprache N1 - Aachen, Techn. Hochsch., Diss., 2013 AB - Infinite two-player games are of interest in computer science since they provide an algorithmic framework for the study of nonterminating reactive systems. Usually, an infinite game is specified by an ω-language containing all winning plays for one of the two players or by a game graph and a winning condition on infinite paths through this graph. Many algorithmic results are known for the case of regular specifications and for finite game graphs with winning conditions like parity or Muller conditions capturing regular objectives. The present thesis offers results that also cover a class of nonregular specifications as well as a class of infinite game graphs, namely those specified by pushdown automata, i.e, we consider contextfree specifications and pushdown game graphs with parity or Muller winning conditions. We extend various central results known for regular games to the class of pushdown games. We focus on the following four questions. Firstly, we analyze how the format of a pushdown winning strategy matches the type of the pushdown game specification. Here, we establish a strong connection between the formats of specifications and formats of corresponding winning strategies for several types of contextfree games, but we also exhibit cases of contextfree games where this correspondence fails. Secondly, we investigate delay games with contextfree winning conditions. In such a game one of the players has the possibility to postpone his moves for some time, thus obtaining a lookahead on the moves of the opponent. We clarify whether the winner of a deterministic contextfree delay game can be determined effectively as well as what amount of lookahead is necessary to win such games. Thirdly, we investigate the synthesis problem for distributed systems which consist of several cooperating components communicating with each other and with the environment. A distributed system is specified by an architecture comprising the communication structure of the system. Here, we study both main concepts, that of global and that of local specifications. We offer a complete characterization of the decidable architectures for local specifications, which may be deterministic contextfree or regular. Moreover, we prove that, for global deterministic contextfree specifications, the distributed synthesis problem is undecidable. Finally, we address the problem whether the winner of an infinite game can be already determined after a finite play prefix. Extending results for the case of finite game graphs, we introduce finite-duration parity pushdown games and establish their completeness for solving parity pushdown games. This yields a new reduction method to determine the winner of a pushdown game by solving a reachability game on a finite game graph. KW - Automatentheorie (SWD) KW - Unendliches Spiel (SWD) KW - Kellerautomat (SWD) KW - Reaktives System (SWD) LB - PUB:(DE-HGF)11 UR - https://publications.rwth-aachen.de/record/210437 ER -