Strategien in unendlichen Spielen mit Liveness-Gewinnbedingungen : Syntheseverfahren, Optimierung und Implementierung

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.

Grantor dc:publisher

Publikationsserver der RWTH Aachen University

Year dc:date

2005

Author dc:creator

• Wallmeier, Nico

Contributors dc:contributor

• Thomas, Wolfgang

• info:eu-repo/classification/ddc/004
• Spieltheorie
• Automatentheorie
• Informatik
• game theorie
• automata theorie

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

ger

Identifier

https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-112529%22

OAI record oai:identifier

https://publications.rwth-aachen.de/oai2d?verb=GetRecord&metadataPrefix=oai_dc&identifier=oai%3Apublications.rwth-aachen.de%3A49961