Making Agents' Abilities Explicit
This work addresses modeling flexibility and intuitive interpretations in multiagent systems, representing an incremental improvement over existing semantic variants.
The authors tackled the issue of varying interpretations in alternating-time temporal logics (ATL/ATL*) by extending Concurrent Game Structures with explicit agents' abilities, resulting in PSACE/2EXPTIME model-checking algorithms and a prototype tool that demonstrates practical feasibility.
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.