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 also 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.

Kurzfassung in Deutsch: Gegenstand dieser Arbeit sind Lösungsverfahren für unendliche Spiele und die Implementierung entsprechender Algorithmen im Rahmen einer Experimentierplattform. Der Schwerpunkt liegt auf Spielen mit Gewinnbedingungen, welche gewisse Liveness-Eigenschaften fordern. Eine für Anwendungen (etwa in der Controller-Synthese) zentrale Liveness-Eigenschaft ist die `Request-Response-Bedingung'. Sie ist eine Konjunktion von Bedingungen der folgenden Gestalt: Immer wenn ein `Request'-Zustand besucht wird, folgt irgendwann später auch der Besuch eines entsprechenden `Response'-Zustandes. Eng verwandt damit sind die sogenannten `Streett-Bedingungen', in denen für wiederholte Besuche gewisser Zustände wiederholte Besuche anderer Zustände gefordert werden. Es werden verschiedene Lösungsverfahren für Request-Response-Spiele und Streett-Spiele vorgestellt, mit Anwendungen etwa in der Analyse von Live-Sequence-Charts. Der Hauptbeitrag besteht in einer quantitativen Analyse der Request-Response-Spiele. Ein natürlicher Ansatz zur quantitativen Abstufung von Gewinnstrategien berücksichtigt die Wartezeiten, die in einer unendlichen Partie zwischen den Besuchen von `Request'- und nachfolgenden `Response'-Zuständen verstreichen. Dazu werden verschiedene Qualitätsmase für Partien in Request-Response-Spielen (über endlichen Spielgraphen) eingeführt und diskutiert. Für Mase, in denen die `Strafe' mehr als linear in den Wartezeiten steigt, wird eine algorithmische Berechnung optimaler Gewinnstrategien vorgestellt. Kernpunkt ist eine Reduktion auf Mean-Payoff-Spiele über endlichen Zustandsräumen, mit der zugleich gezeigt wird, dass optimale Strategien durch endliche Automaten implementierbar sind. Die Experimentierplattform GaSt (`Games, Automata \& Strategies') integriert zahlreiche Algorithmen zur Theorie der Omega-Automaten und zur Lösung unendlicher Spiele.

Abstract in english: In this thesis we develop methods for the solution of infinite games and present implementations of corresponding algorithms in the framework of a platform for the experimental study of automata theoretic algorithms. Our focus is on games with winning conditions that express certain liveness properties. A central type of liveness requirement in applications (e.g., in controller synthesis) is the ``request-response condition''. It has the form of a conjunction of conditions ``Whenever a `request'-state is visited, sometime later a corresponding `response'-state is visited''. A closely related winning condition is the ``Streett condition'' in which for repeated visits of certain states the repeated visits of other states is required. We present methods for the solution of request-response games and Streett games, the latter with an application in the analysis of live-sequence-charts. The main contribution is a quantitative analysis of request-response games. We pursue a natural approach for the quantitative evaluation of winning strategies by taking into account the waiting times that elapse between visits of ``request''-states and subsequent visits of ``response''-states in an infinite play. We introduce and discuss several related measures of plays in request-response games (over finite game arenas). For measures that induce a ``penalty'' which grows more than linearly in the waiting times, we present an algorithm to compute optimal winning strategies. The core of the argument is a reduction to mean-payoff games over finite arenas; it also shows that optimal strategies are implementable by finite-state machines. The experimental platform GaSt (``Games, Automata & Strategies'') offers numerous algorithms of the theory of omega-automata and for the solution of infinite games.

The two determinization procedures of Safra and Muller-Schupp for Büchi automata are compared, based on an implementation in a program called OmegaDet.

The two determinization procedures of Safra and Muller-Schupp for Büchi automata are compared, based on an implementation in a program called OmegaDet.

We present a method to solve certain infinite games over finite state spaces and apply this for the automatic synthesis of finite-state controllers. A lift-controller problem serves as an example for which the implementation of our algorithm has been tested. The specifications consist of safety conditions and so-called ``request-response-conditions'' (which have the form ``after visiting a state of P later a state of R is visited''). Many real-life problems can be modeled in this framework. We sketch the theoretical solution which synthesizes a finite-state controller for satisfiable specifications. The core of the implementation is a convenient input language (based on enriched Boolean logic) and a realization of the abstract algorithms with OBDD's (ordered binary decision diagrams).