Reasoning about coalitional ability in games: Coalition Logic vs. PDL
报告人：Thomas Ågotnes (挪威卑尔根大学教授）
报告简介： The use of modal logics for reasoning about games has been of considerable interest in recent years. One popular framework is Pauly’s coalition logic (CL), developed to reason about coalitional abilities of the form “coalition C have the ability to make formula phi true no matter what the other agents do”. CL can be seen as the next-time fragment of Alternating-time temporal logic (ATL). Another framework is propositional dynamic logic (PDL), which, although developed to reason about the execution of computer programs, can also be used to reason about games. In this talk, I will discuss some aspects of the relationship between the two, in particular how PDL can be used to reason about coalitional ability. An advantage of PDL over CL is that it is a standard, normal, modal logic. There is a restriction to this approach: it can only be used to reason about game structures that are injective. I will discuss consequences on this restriction, in particular for the so-called playability properties of effectivity functions, and present a variant of Pauly’s representation theorem for effectivity functions of injective games. The talk is based on joint work with Natasha Alechina.