Special LIRa session on Logic and Strategies in Groningen

A well known result by Marc Pauly states that for every playable effectivity function E there exists a strategic game that assigns to coalitions exactly the same power as E, and vice versa. While the latter direction of the correspondence is correct, I will show that the former is not. I will discuss the consequences of this problem, especially for the logics used to reason on strategic games. I will then characterize the class of ‘truly playable’ effectivity functions, that does correspond to strategic games. I will also show that Coalition Logic is not expressive enough to distinguish between playable and truly playable effectivity functions, and I will extend it to a logic that can make this distinction while enjoying finite axiomatization and finite model property. What I present is joint work with Valentin Goranko (University of Denmark) and Wojtek Jamroga (University of Luxembourg).

Model checking games present one of the classic applications of game theoretic techniques in logic. In this view, the notion of truth can be stated in terms of winning strategies. Efficient algorithms to find the winning region in the associated class of games can in turn be employed to solve the model checking question. There is also the reverse relationship between games and logic: the question of whether the winning region (and the winning strategy) of a class of games is definable in a logic.

It is well known that the class of perfect information games with omega regular objectives encompass model checking games of several interesting logics including modal logic, first order logic and its fixed point extensions. It is well behaved in terms of computational and logical definability questions and also robust in the sense that these properties remain invariant under natural extensions. However, moving to the class of imperfect information games, most of the nice algorithmic and definability properties break down. We look at a natural subclass of imperfect information games for which the computational questions remain tractable.

This talk presents an attempt to bridge the gap between logical and cognitive treatments of strategic reasoning in games. The focus is backward induction, a principle which is purported to follow from common knowledge of rationality by Zermelo’s theorem. There have been extensive formal debates about the merits of the principle of backward induction among game theorists and logicians. Experimental economists and psychologists have shown that human subjects, perhaps due to their bounded resources, do not always follow the backward induction strategy, leading to unexpected outcomes. Recently, based on an eye-tracker study by Ben Meijering, it has turned out that even human subjects who produce the outwardly correct ‘backward induction answer’ may use a different internal reasoning strategy to achieve it. This paper presents a formal language to represent different strategies on a finer-grained level than was possible before. The language and its semantics may lead to precisely distinguishing different cognitive reasoning strategies, that can then be tested on the basis of computational cognitive models and experiments with human subjects. This talk is based on work with Ben Meijering and Sujata Ghosh.