Games and logical expressiveness

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.

Grantor dc:publisher

Publikationsserver der RWTH Aachen University

Year dc:date

2005

Author dc:creator

• Berwanger, Dietmar

Contributors dc:contributor

• Grädel, Erich

• info:eu-repo/classification/ddc/510
• Spieltheorie
• My-Kalkül
• Mathematik
• Logik
• Interaktive Systeme

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

eng

Identifier

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

OAI identifier oai:identifier

oai:publications.rwth-aachen.de:58934