Seminar session on Strategies on Monday October 26th

We argue that ATL is too weak to express several important multi-agent system verification properties. In particular, many important aspects of agent interaction cannot be suitably modeled in ATL since it lacks the possibility to talk about strategies more explicitly and, in particular, reason conditionally on strategy performance. Our answer to this observation (that is also made by several other authors) will be to extend ATL with stit-reasoning capability. We extend the basic interactive reasoning objective of ATL, as expressed by the super-additivity axiom, and enable assumption-guarantee type reasoning, stit-reasoning, etc. We present a general semantics, which is not finitely axiomatizable and then focus on suitable fragments that are. Also, we compare the logic’s suitability for multi-agent system verification with verification formalisms based on dynamic logic. We will give a number of arguments in favor of stit-formalisms. But, which paradigm to use ultimately depends on what kind of properties we want to verify.

Logical analyses of games typically consider players’ strategies as atomic objects and the reasoning is about existence of strategies, rather than about 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.

We propose a syntactic framework in which strategies are constructed in a structural manner and show how explicit reasoning of strategies can be achieved. We also look at how structurally specified strategies can be adapted to the case where the game itself has compositional structure. We suggest that rather than analyzing the composite game, one needs to compose game-strategy pairs in order to reason about strategic response of players. We consider a propositional dynamic logic whose programs are regular expressions over such game-strategy pairs and present a complete axiomatization of the logic.

In this talk, we first show that Parikh’s Game Logic framework gives a syntax for explicit strategies as well, providing a complete axiomatization of the resulting logic for games and strategies, and then explore its relationship with different kinds of logic games. Along the way, we try to find an answer to the following question, ”from the logical point of view, what do we really gain by adding explicit strategies in the game logic framework?”