Alternating-time Temporal Logic with Stochastic Abilities

Multi-agent systems strategic verification is a branch of formal methods to model, reason about, and verify strategic behavior in complex environments. The notion of agent capacity was introduced alongside the strategic logic CapATL to model multi-agent systems in which each player may exhibit diverse abilities or profiles. These capacities can represent various aspects, such as an agent's experience level, personality traits, type, or version. In real-world applications, domain knowledge or prior statistical analyses may provide a probability distribution over the possible profiles of each agent. This leads to the concept of stochastic abilities, where capacities are assigned probabilistically, yet remain private to other agents. In this context, we introduce a novel probabilistic strategic logic, called ATL-SA, that allows the expression of properties concerning the likelihood that agents or coalitions can achieve specific temporal objectives under uncertainty about their capacities. We study the upper and lower complexity bounds of ATL-SA model checking and demonstrate its practical applicability through a use case in cybersecurity, showcasing its potential for analysing systems with probabilistic agent profiles.