Optimal Strategy Synthesis in Request-Response Games
We show the solvability of an optimization problem on infinite two-player games. The winning conditions are of the “request-response” format, i.e. conjunctions of conditions of the form “if a state with property Q is visited, then later a state with property P is visited”. We ask for solutions that do not only guarantee the satisfaction of such conditions but also minimal wait times between visits to Q-states and subsequent visits to P-states. We present a natural class of valuations of infinite plays that captures this optimization problem, and with respect to this measure show the existence of an optimal winning strategy (if a winning strategy exists at all) and that it can be realized by a finite-state machine. For the latter claim we use a reduction to the solution of mean-payoff games due to Paterson and Zwick.
KeywordsWait Time Temporal Logic Memory State Path Segment Linear Time Temporal Logic
Unable to display preview. Download preview PDF.
- 5.Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. Math. 35, 413–422Google Scholar
- 6.Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. Int. J. of Game Theory 8, 109–113Google Scholar
- 12.McNaughton, R.: Playing infinite games in finite time. In: Salomaa, A., Wood, D., Yu, S. (eds.) A Half-Century of Automata Theory, pp. 73–91. World Scientific, Singapore (2000)Google Scholar
- 14.Wallmeier, N.: Strategien in unendlichen Spielen mit Liveness-Gewinnbedingungen: Syntheseverfahren, Optimierung und Implementierung, Dissertation, RWTH Aachen (2007)Google Scholar