But there are also surprising exceptions to that rule, e.g., generalized reachability games. For most conditions in the literature, tight bounds are known, see, e.g. Nowadays, one of the most basic questions about a given winning condition is that about such upper and lower bounds. In particular, the seminal work by Dziembowski, Jurdziński, and Walukiewicz addressed the problem of determining upper and lower bounds on the size of finite-state winning strategies in games with Muller winning conditions. These facts explain the need for studying the existence and properties of finite-state strategies in infinite games. Also, our framework is more abstract and therefore applicable to a wider range of acceptance conditions (e.g., qualitative ones) and yields in general smaller strategies, but there are of course some similarities, which we discuss in detail. In comparison to Salzmann’s notion, where strategies syntactically depend on a given automaton representing the winning condition, our strategies are independent of the representation of the winning condition and therefore more general. However, this is offset by the fact that strategies of the second type are simpler to compute than the delay-oblivious ones and have overall fewer states, if the lookahead is large. In particular, the number of states of the delay-aware strategies is independent of the size of the lookahead, but often larger in the size of the automaton recognizing the winning condition. We discuss this issue in-depth in Sections 3 and 5 by proposing two notions of finite-state strategies, a delay-oblivious one which yields large strategies in the size of the lookahead, and a delay-aware one that follows naturally from the reductions to Gale-Stewart games mentioned earlier. However, the exact nature of finite-state strategies in delay games is not as canonical as for Gale-Stewart games. Indeed, in his master’s thesis, Salzmann recently introduced the first notion of finite-state strategies in delay games and, using these reductions, presented an algorithm computing them for several types of acceptance conditions, e.g., parity conditions and related ω-regular ones. These reductions and the fact that finite-state strategies suffice for the games obtained in the reductions imply that (some kind of) finite-state strategies exist. In fact, all these proofs rely on the same basic construction that was already present in the work of Holtmann, Kaiser, and Thomas, i.e., a reduction to a Gale-Stewart game using equivalence relations that capture the behavior of the automaton recognizing the winning condition. Furthermore, for all those winning conditions, the winner of a delay game can be determined effectively. On the other hand, it is known that bounded lookahead suffices for many winning conditions of importance, e.g., the ω-regular ones, those recognized by parity and Streett automata with costs, and those definable in (parameterized) linear temporal logics. However, those restrictions are concerned with the amount of information about the lookahead’s evolution a strategy has access to, and do not restrict the size of the strategies: In general, they are still infinite objects. In previous work, restricted classes of strategies for delay games have been considered. Finally, the uniformization problem for relations over infinite words boils down to solving delay games: a relation L ⊆ ( Σ I × Σ O ) ω is uniformized by a continuous function (in the Cantor topology) if, and only if, the delaying player wins the delay game with winning condition L. Furthermore, Martin’s seminal Borel determinacy theorem for Gale-Stewart games has been lifted to delay games and winning conditions beyond the ω-regular ones have been investigated. Forty years later, delay games were revisited by Holtmann, Kaiser, and Thomas and the first comprehensive study was initiated, which settled many basic problems like the exact complexity of solving ω-regular delay games and the amount of lookahead necessary to win such games.
TRIVIAL FINITE STATE AUTOMATA HOW TO
Büchi and Landweber had shown how to solve infinite two-player games with ω-regular winning conditions. Delay games have recently received a considerable amount of attention after being introduced by Hosch and Landweber only three years after the seminal Büchi-Landweber theorem.
0 kommentar(er)
