The frontier between decidability and undecidability for logics for strategic reasoning in the presence of imperfect information

Speaker:  Catalin Dima (Université Paris-Est Créteil.)

Abstract:

The last 15-20 years have seen a number of logical formalisms that focus on strategic reasoning. These logics aim at giving specification languages for various multi-agent game structures, in which agents have adversarial or cooperative objectives which may be qualitative or quantitative and may have various types of imperfect information. The presence of imperfect information raises a particular difficulty in that many games cannot be solved algorithmically, as well as their corresponding logical formalisms. In this tutorial I will review some techniques for proving that the Alternating-time Temporal Logic has an undecidable model-checking problem, but this problem becomes decidable when considering memoryless strategies, coalitions with distributed knowledge, hierarchical knowledge and public or coalition-public announcements. I will also give a short introduction to the model-checking tool MCMAS which relies on the memoryless semantics for ATL with imperfect information, and the problems that arise when implementing the model-checking algorithms for this case.