{"id":{"repo_id":"aachen","oai_identifier":"oai:publications.rwth-aachen.de:58934"},"canonical_url":"https://search.dev.ndltd.org/etd/aachen/oai:publications.rwth-aachen.de:58934","repository":{"repo_id":"aachen","name":"RWTH Aachen University","base_url":"https://publications.rwth-aachen.de/oai2d"},"display":{"title":"Games and logical expressiveness","abstract":"For the study of interactive systems, game theory provides a framework of versatile models and intuitive languages to abstract from the intricacies of distributed control. The effectiveness of this framework relies on logical foundations that allow rigorous specification and reasoning in terms of mathematical structures and formal languages. In view of their aims, logic and games are therefore strongly correlated. Nevertheless, regarding their inner structure, there is a large gap dividing the two paradigms. In our contribution, we take a step towards bridging this gap. We develop a game that captures crucial issues of descriptive and computational complexity of the mu-calculus, a very powerful specification logic. As a first application, we address the model-checking problem for the mu-calculus, an issue of controversial algorithmic complexity, and show that our game naturally leads to instances that can be solved in polynomial time. On the basis of this game, we further derive a parameter that measures the syntactic resources required to specify the behaviour of a given transition system. As a consequence, it follows that the expressive power of the mu-calculus strictly increases with the number of variables used in formulae. Already a particular case of this result, that three variables can express more than two, answers an open question from 1983 regarding the expressive power of Parikh's Game Logic.","abstract_html":"For the study of interactive systems, game theory provides a framework of versatile models and intuitive languages to abstract from the intricacies of distributed control. The effectiveness of this framework relies on logical foundations that allow rigorous specification and reasoning in terms of mathematical structures and formal languages. In view of their aims, logic and games are therefore strongly correlated. Nevertheless, regarding their inner structure, there is a large gap dividing the two paradigms. In our contribution, we take a step towards bridging this gap. We develop a game that captures crucial issues of descriptive and computational complexity of the mu-calculus, a very powerful specification logic. As a first application, we address the model-checking problem for the mu-calculus, an issue of controversial algorithmic complexity, and show that our game naturally leads to instances that can be solved in polynomial time. On the basis of this game, we further derive a parameter that measures the syntactic resources required to specify the behaviour of a given transition system. As a consequence, it follows that the expressive power of the mu-calculus strictly increases with the number of variables used in formulae. Already a particular case of this result, that three variables can express more than two, answers an open question from 1983 regarding the expressive power of Parikh's Game Logic.","abstract_has_math":false,"creators":["Berwanger, Dietmar"],"institution":"Publikationsserver der RWTH Aachen University","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Grädel, Erich"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2005,"date_issued":"2005","date_published":"2005","updated_at":"2026-07-30T19:42:31Z","subjects":["info:eu-repo/classification/ddc/510","Spieltheorie","My-Kalkül","Mathematik","Logik","Interaktive Systeme"],"languages":["eng"],"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-120760%22"],"render_values":[{"text":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-120760%22","href":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-120760%22","code":true}]}]},"links":{"outbound_url":"https://publications.rwth-aachen.de/record/58934","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Grädel, Erich"]},{"key":"dc:creator","label":"Author","values":["Berwanger, Dietmar"]}]},{"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-20050936"]},{"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/510","Spieltheorie","My-Kalkül","Mathematik","Logik","Interaktive Systeme"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"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/58934","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-120760%22"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["For the study of interactive systems, game theory provides a framework of versatile models and intuitive languages to abstract from the intricacies of distributed control. The effectiveness of this framework relies on logical foundations that allow rigorous specification and reasoning in terms of mathematical structures and formal languages. In view of their aims, logic and games are therefore strongly correlated. Nevertheless, regarding their inner structure, there is a large gap dividing the two paradigms. In our contribution, we take a step towards bridging this gap. We develop a game that captures crucial issues of descriptive and computational complexity of the mu-calculus, a very powerful specification logic. As a first application, we address the model-checking problem for the mu-calculus, an issue of controversial algorithmic complexity, and show that our game naturally leads to instances that can be solved in polynomial time. On the basis of this game, we further derive a parameter that measures the syntactic resources required to specify the behaviour of a given transition system. As a consequence, it follows that the expressive power of the mu-calculus strictly increases with the number of variables used in formulae. Already a particular case of this result, that three variables can express more than two, answers an open question from 1983 regarding the expressive power of Parikh's Game Logic."]},{"key":"dc:source","label":"Dc Source","values":["Aachen : Publikationsserver der RWTH Aachen University VIII, 111 S. : graph. Darst. (2005). = Aachen, Techn. Hochsch., Diss., 2005"]},{"key":"dc:title","label":"Title","values":["Games and logical expressiveness"]}]}],"canonical_facts":{"dc:contributor":["Grädel, Erich"],"dc:coverage":["DE"],"dc:creator":["Berwanger, Dietmar"],"dc:date":["2005"],"dc:description":["For the study of interactive systems, game theory provides a framework of versatile models and intuitive languages to abstract from the intricacies of distributed control. The effectiveness of this framework relies on logical foundations that allow rigorous specification and reasoning in terms of mathematical structures and formal languages. In view of their aims, logic and games are therefore strongly correlated. Nevertheless, regarding their inner structure, there is a large gap dividing the two paradigms. In our contribution, we take a step towards bridging this gap. We develop a game that captures crucial issues of descriptive and computational complexity of the mu-calculus, a very powerful specification logic. As a first application, we address the model-checking problem for the mu-calculus, an issue of controversial algorithmic complexity, and show that our game naturally leads to instances that can be solved in polynomial time. On the basis of this game, we further derive a parameter that measures the syntactic resources required to specify the behaviour of a given transition system. As a consequence, it follows that the expressive power of the mu-calculus strictly increases with the number of variables used in formulae. Already a particular case of this result, that three variables can express more than two, answers an open question from 1983 regarding the expressive power of Parikh's Game Logic."],"dc:identifier":["https://publications.rwth-aachen.de/record/58934","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-120760%22"],"dc:language":["eng"],"dc:publisher":["Publikationsserver der RWTH Aachen University"],"dc:relation":["info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-20050936"],"dc:rights":["info:eu-repo/semantics/openAccess"],"dc:source":["Aachen : Publikationsserver der RWTH Aachen University VIII, 111 S. : graph. Darst. (2005). = Aachen, Techn. Hochsch., Diss., 2005"],"dc:subject":["info:eu-repo/classification/ddc/510","Spieltheorie","My-Kalkül","Mathematik","Logik","Interaktive Systeme"],"dc:title":["Games and logical expressiveness"],"dc:type":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]},"updated_at":"2026-07-30T19:42:31Z"}