Making Agents' Abilities Explicit

Alternating-time temporal logics (ATL/ATL*) represent a family of modal logics for reasoning about agents' strategic abilities in multiagent systems (MAS). The interpretations of ATL/ATL* over the semantic model Concurrent Game Structures (CGS) usually vary depending on the agents' abilities, for instance, perfect vs. imperfect information, perfect vs. imperfect recall, resulting in a variety of variants which have been studied extensively in literature. However, they are defined at the semantic level, which may limit modeling flexibilities and may give counter-intuitive interpretations. To mitigate these issues, in this work, we propose to extend CGS with agents' abilities and study the new semantics of ATL/ATL* under this model. We give PSACE/2EXPTIME model-checking algorithms for ATL/ATL* and implement them as a prototype tool. Experiment results show the practical feasibility of the approach.