{"id":{"repo_id":"aachen","oai_identifier":"oai:publications.rwth-aachen.de:56433"},"canonical_url":"https://search.dev.ndltd.org/etd/aachen/oai:publications.rwth-aachen.de:56433","repository":{"repo_id":"aachen","name":"RWTH Aachen University","base_url":"https://publications.rwth-aachen.de/oai2d"},"display":{"title":"Strategiesynthese für Paritätsspiele auf endlichen Graphen","abstract":"Parity games are infinite two person games, here considered on finite graphs. A play is an infinite path in the graph, whose vertices are chosen by the two players in alternation. The winner of the play is determined by the vertices that are visited infinitely often in the play. The problem of solving a parity game (i.e., finding the winner for plays starting in a given vertex and the construction of a winning strategy) belongs to the complexity class NP intersection co-NP. It is one of the core problems in the theory of program verification, because many model checking problems can be reduced to solving parity games by a polynomial time reduction. In this thesis a new algorithm for solving parity games is presented. Contrary to known discrete procedures this one uses the method of strategy improvement as it is already known from stochastic games. Unlike for procedures in the literature, no example is known for the present algorithm which requires polynomial time. The algorithm is based on a new kind of valuation for infinite plays.","abstract_html":"Parity games are infinite two person games, here considered on finite graphs. A play is an infinite path in the graph, whose vertices are chosen by the two players in alternation. The winner of the play is determined by the vertices that are visited infinitely often in the play. The problem of solving a parity game (i.e., finding the winner for plays starting in a given vertex and the construction of a winning strategy) belongs to the complexity class NP intersection co-NP. It is one of the core problems in the theory of program verification, because many model checking problems can be reduced to solving parity games by a polynomial time reduction. In this thesis a new algorithm for solving parity games is presented. Contrary to known discrete procedures this one uses the method of strategy improvement as it is already known from stochastic games. Unlike for procedures in the literature, no example is known for the present algorithm which requires polynomial time. The algorithm is based on a new kind of valuation for infinite plays.","abstract_has_math":false,"creators":["Vöge, Jens"],"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":2000,"date_issued":"2000","date_published":"2000","updated_at":"2026-07-30T19:41:53Z","subjects":["info:eu-repo/classification/ddc/004","Informatik","Unendliches Spiel","Zweipersonenspiel","Endlicher Graph"],"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-118538%22"],"render_values":[{"text":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-118538%22","href":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-118538%22","code":true}]}]},"links":{"outbound_url":"https://publications.rwth-aachen.de/record/56433","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%3A56433","prefix":"oai_dc"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Thomas, Wolfgang"]},{"key":"dc:creator","label":"Author","values":["Vöge, Jens"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:coverage","label":"Dc Coverage","values":["DE"]},{"key":"dc:date","label":"Dc Date","values":["2000"]},{"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-1282"]},{"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","Informatik","Unendliches Spiel","Zweipersonenspiel","Endlicher Graph"]}]},{"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/56433","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-118538%22"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Parity games are infinite two person games, here considered on finite graphs. A play is an infinite path in the graph, whose vertices are chosen by the two players in alternation. The winner of the play is determined by the vertices that are visited infinitely often in the play. The problem of solving a parity game (i.e., finding the winner for plays starting in a given vertex and the construction of a winning strategy) belongs to the complexity class NP intersection co-NP. It is one of the core problems in the theory of program verification, because many model checking problems can be reduced to solving parity games by a polynomial time reduction. In this thesis a new algorithm for solving parity games is presented. Contrary to known discrete procedures this one uses the method of strategy improvement as it is already known from stochastic games. Unlike for procedures in the literature, no example is known for the present algorithm which requires polynomial time. The algorithm is based on a new kind of valuation for infinite plays."]},{"key":"dc:source","label":"Dc Source","values":["Aachen : Publikationsserver der RWTH Aachen University 131 S. : graph. Darst. (2000). = Aachen, Techn. Hochsch., Diss., 2000"]},{"key":"dc:title","label":"Title","values":["Strategiesynthese für Paritätsspiele auf endlichen Graphen"]}]}],"canonical_facts":{"dc:contributor":["Thomas, Wolfgang"],"dc:coverage":["DE"],"dc:creator":["Vöge, Jens"],"dc:date":["2000"],"dc:description":["Parity games are infinite two person games, here considered on finite graphs. A play is an infinite path in the graph, whose vertices are chosen by the two players in alternation. The winner of the play is determined by the vertices that are visited infinitely often in the play. The problem of solving a parity game (i.e., finding the winner for plays starting in a given vertex and the construction of a winning strategy) belongs to the complexity class NP intersection co-NP. It is one of the core problems in the theory of program verification, because many model checking problems can be reduced to solving parity games by a polynomial time reduction. In this thesis a new algorithm for solving parity games is presented. Contrary to known discrete procedures this one uses the method of strategy improvement as it is already known from stochastic games. Unlike for procedures in the literature, no example is known for the present algorithm which requires polynomial time. The algorithm is based on a new kind of valuation for infinite plays."],"dc:identifier":["https://publications.rwth-aachen.de/record/56433","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-118538%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-1282"],"dc:rights":["info:eu-repo/semantics/openAccess"],"dc:source":["Aachen : Publikationsserver der RWTH Aachen University 131 S. : graph. Darst. (2000). = Aachen, Techn. Hochsch., Diss., 2000"],"dc:subject":["info:eu-repo/classification/ddc/004","Informatik","Unendliches Spiel","Zweipersonenspiel","Endlicher Graph"],"dc:title":["Strategiesynthese für Paritätsspiele auf endlichen Graphen"],"dc:type":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]},"updated_at":"2026-07-30T19:41:53Z"}