Multi-agent systems describe interactions of multiple entities called agents, often assumed to be intelligent and autonomous. Alternating-time temporal logic (ATL*) and its fragment ATL are logics which allow for reasoning about strategic interactions in such systems, by extending the framework of temporal logic with the game-theoretic notion of strategic ability. While model checking of ATL under perfect information seems to be feasible in practice, model checking of ATL under imperfect information is still applicable only to small and medium size systems.
This lecture is about selected approaches which can make model checking ATL*, ATL and its discrete time extension TATL more efficient. We start with multi-valued versions of ATL* and show the general method for translation from multi-valued to two-valued model checking. Next, we investigate ATL* without the next step operator, interpreted in asynchronous systems and show that for memoryless imperfect information contrary to memoryless perfect information, one can apply partial order reduction methods. Finally, we build a hierarchy of strategies for TATL comparing the expressive power of the logic against ATL and discuss a possible impact of this hierarchy on improving efficiency of model checking TATL