Capacity ATL

TL;DR

This paper introduces a new framework for modeling agents with varying capacities in multi-agent systems, extending logic to analyze strategic abilities under imperfect information.

Contribution

It defines a novel class of concurrent game structures with capacity-modified actions and extends ATL to reason about these complex multi-agent scenarios.

Findings

Formal definition of capacity-based game structures

Extension of ATL for capacity reasoning

Application to heterogeneous multi-agent systems

Abstract

Model checking strategic abilities was successfully developed and applied since the early 2000s to ensure properties in Multi-Agent System. In this paper, we introduce the notion of capacities giving different abilities to an agent. This applies naturally to systems where multiple entities can play the same role in the game, such as different client versions in protocol analysis, different robots in heterogeneous fleets, different personality traits in social structure modeling, or different attacker profiles in a cybersecurity setting. With the capacity of other agents being unknown at the beginning of the game, the longstanding problems of imperfect information arise. Our contribution is the following: (i) we define a new class of concurrent game structures where the agents have different capacities that modify their action list and (ii) we introduce a logic extending Alternating-time Temporal Logic to reason about these games.