A Logical Study of Strategies in Games [HBNI Th15]

Abstract

The Main theme of this thesis is reasoning about strategies in games in logical framework. Logical analyses of games typically consider players' strategies as atomic objects and the reasoning is about existence of strategies themselves. This works well with the underlying assumption that players are rational and possess unbounded computational ability. However, in many practical situations players have limited computational resources. Thus a prescriptive theory which provides advice to players needs to view strategies as relations constraining players moves rather than view them as complete functions. The central idea is to formulate the notion of composite strategies which are constructed in a structural manner and show how explicit reasoning of strategies can be achieved. The first part of the thesis looks at a logical analysis of strategies. The notion of structurally specified strategies in the framework of unbounded duration games on graphs is defined. This enables to reason about how a player's strategy may depend on assumptions about the opponent's strategy. Such specifications give rise to partially specified bounded memory strategies. A simple modal logic is considered to reason about the structured strategies. A complete axiomatization of this logic and show that the truth checking problem of the logic is decidable. Then structurally specified strategies are viewed for adaptations to the case where the game itself has compositional structure. It is suggested that, rather than performing strategic reasoning on the composite game one needs to compose game-strategy pairs. The advantage of imposing structure not merely on games or on strategies, but on game-strategy pairs, is that one can speak of a composite game g followed by g' whereby if the opponent played a strategy "Pie" in g, the player responds with sigma in g' to ensure a certain outcome. In the presence of iteration, a player has significant ability to strategize by taking into account the explicit structure of games. A propositional dynamic logic is considered whose programs are regular expressions over such game-strategy pairs and present a complete axiomatization of the logic. It is also shown that the satisfiability problem of the logic is decidable. An algorithmic analysis of games is considered in the second part of the thesis. "Evaluation Automata" is proposed as a convenient finite state model to present the preference orderings of players in infinite games. The classical solution concept of Nash equilibrium is considered in terms of functional strategies and shown that an equilibrium profile always exists in infinite duration games on finite arenas where the preference orderings of players are specified in terms of evaluation automata. It is also shown that the best response verification question is decidable with respect to strategy specifications and that synthesizing a best response strategy is possible. All the above mentioned analyses are carried out for games of perfect information. Finally multi-player games of imperfect information is investigated. As per the results of Peterson and Reif(1979), The verification question in general asks, whether a subset of players have a distributed winning strategy is undecidable in these games. The crucial element which yields undecidability is the fact that players are not allowed to communicate with each other. A framework is proposed to model games of imperfect information where communication is explicitly represented. A player's information partition is generated in a structural manner rather than being presented as part of the game formalism. It is shown that the subclass of games where communication is restricted to public announcements the verification question is decidable. Also the non-zero sum version is analysed where players have preference orderings over outcomes. It is shown that the best response computation can be performed and that one can verify whether a strategy profile constitutes an equilibrium can be carried out.