{"id":{"repo_id":"aachen","oai_identifier":"oai:publications.rwth-aachen.de:49961"},"canonical_url":"https://search.dev.ndltd.org/etd/aachen/oai:publications.rwth-aachen.de:49961","repository":{"repo_id":"aachen","name":"RWTH Aachen University","base_url":"https://publications.rwth-aachen.de/oai2d"},"display":{"title":"Strategien in unendlichen Spielen mit Liveness-Gewinnbedingungen : Syntheseverfahren, Optimierung und Implementierung","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Wallmeier, Nico"],"institution":"Publikationsserver der RWTH Aachen University","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Thomas, Wolfgang"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2005,"date_issued":"2005","date_published":"2005","updated_at":"2026-07-30T19:40:16Z","subjects":["info:eu-repo/classification/ddc/004","Spieltheorie","Automatentheorie","Informatik","game theorie","automata theorie"],"languages":["ger"],"rights":["info:eu-repo/semantics/openAccess"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-112529%22"],"render_values":[{"text":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-112529%22","href":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-112529%22","code":true}]}]},"links":{"outbound_url":"https://publications.rwth-aachen.de/record/49961","outbound_label":"Repository record","outbound_source":"dc:identifier"},"source_record":{"url":"https://publications.rwth-aachen.de/oai2d?verb=GetRecord&metadataPrefix=oai_dc&identifier=oai%3Apublications.rwth-aachen.de%3A49961","prefix":"oai_dc"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Thomas, Wolfgang"]},{"key":"dc:creator","label":"Author","values":["Wallmeier, Nico"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:coverage","label":"Dc Coverage","values":["DE"]},{"key":"dc:date","label":"Dc Date","values":["2005"]},{"key":"dc:publisher","label":"Institution","values":["Publikationsserver der RWTH Aachen University"]},{"key":"dc:relation","label":"Dc Relation","values":["info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-opus-21296"]},{"key":"dc:type","label":"Dc Type","values":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["info:eu-repo/classification/ddc/004","Spieltheorie","Automatentheorie","Informatik","game theorie","automata theorie"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["ger"]},{"key":"dc:rights","label":"Dc Rights","values":["info:eu-repo/semantics/openAccess"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://publications.rwth-aachen.de/record/49961","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-112529%22"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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."]},{"key":"dc:source","label":"Dc Source","values":["Aachen : Publikationsserver der RWTH Aachen University IV, 138 S. : Ill., graph. Darst. (2005). = Aachen, Techn. Hochsch., Diss., 2005"]},{"key":"dc:title","label":"Title","values":["Strategien in unendlichen Spielen mit Liveness-Gewinnbedingungen : Syntheseverfahren, Optimierung und Implementierung"]}]}],"canonical_facts":{"dc:contributor":["Thomas, Wolfgang"],"dc:coverage":["DE"],"dc:creator":["Wallmeier, Nico"],"dc:date":["2005"],"dc:description":["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."],"dc:identifier":["https://publications.rwth-aachen.de/record/49961","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-112529%22"],"dc:language":["ger"],"dc:publisher":["Publikationsserver der RWTH Aachen University"],"dc:relation":["info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-opus-21296"],"dc:rights":["info:eu-repo/semantics/openAccess"],"dc:source":["Aachen : Publikationsserver der RWTH Aachen University IV, 138 S. : Ill., graph. Darst. (2005). = Aachen, Techn. Hochsch., Diss., 2005"],"dc:subject":["info:eu-repo/classification/ddc/004","Spieltheorie","Automatentheorie","Informatik","game theorie","automata theorie"],"dc:title":["Strategien in unendlichen Spielen mit Liveness-Gewinnbedingungen : Syntheseverfahren, Optimierung und Implementierung"],"dc:type":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]},"updated_at":"2026-07-30T19:40:16Z"}