Strategic Reasoning under Capacity-constrained Agents

Personality traits, experience level, or physical characteristics can affect the capacity (or profile) of an agent. For instance, a basketball player may be right-handed or left-handed, and these two versions cannot do the same actions. Dribbling past the player may require, first, understanding its handedness and, accordingly, execute a trick. Generally, capacities apply to systems where multiple entities can play the same role in the system, 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 cybersecurity. With the capacity of other agents being unknown at the system's initialization, the hardness of imperfect information arises. Our contributions are: (i) introducing Capacity Alternating-time Temporal Logic (CapATL) to reason about concurrent game structure where agents are bounded to capacities, (ii) a model-checking algorithm for CapATL, and (iii) a case study of adaptive honeypot design for cyber deception.