Probabilistic Alternating-Time Temporal Logic with Stochastic Abilities

Model checking provides a rigorous means to analyze complex systems by ensuring properties hold across all executions. While originally applied to closed systems, model checking now extends to multi-agent systems, such as distributed protocols, communication systems, robotics, and cybersecurity. A recurring challenge across these domains is reasoning about agents with hidden and uncertain profiles; for example adversarial traders in markets, coordinated users in social media, or attackers in cybersecurity. Addressing this requires logics capable of capturing both probabilistic profiling and reasonig. Alternating-time Temporal Logic (ATL) offers a foundation for reasoning about strategic abilities in multi-agent systems. Extensions such as ATL with Stochastic Abilities (ATL-SA) incorporate stochastic capacities, but existing frameworks remain limited: they can model uncertainty over profiles or allow reasoning about capacities from observed actions, yet not both simultaneously. In this work, we extend ATL-SA with a probabilistic capacity operator, enabling the specification and verification of properties that combine stochastic profiling, inference of hidden information, and strategic reasoning. This framework broadens the scope of formal verification as a general methodology for adversarial and uncertain environments, with applications spanning markets, social platforms, distributed computing, and cybersecurity.