Making Agents' Abilities Explicit

Alternating-time temporal logics (ATL/ATL*) represent a family of modal and temporal logics for reasoning about strategic abilities of agents in multiagent systems. These logics are usually interpreted over concurrent game structures (CGSs), and their interpretations may vary depending on the abilities of agents, such as perfect versus imperfect information and perfect versus imperfect recall. These different abilities lead to a variety of variants that have been studied extensively in the literature. However, all of these variants are defined at the semantic level, which may restrict modeling flexibility, or even give counterintuitive interpretations. For example, an agent may have different abilities when achieving two different goals on the same CGS. To mitigate these issues, in this paper, we propose to extend CGSs with agents' abilities, resulting in Abilities Augmented CGSs, where concrete abilities can be defined at the syntactic level. We study ATL/ATL* over this new model. We give formal definitions of the new semantics and present model-checking algorithms for ATL/ATL*. We also identify the computational complexity of ATL/ATL* model checking problem, i.e., Delta(P)(3)-/2EXPTIME-complete. The model-checking algorithms are implemented in a prototype tool. The experimental results show the practical feasibility and effectiveness of our approach.