Abstract
Resource-bounded alternating-time temporal logic
(RB-ATL) [Alechina et al., 2010], an extension of
Coalition Logic (CL) and Alternating-time Temporal Logic (ATL), allows reasoning about resource requirements of coalitions in concurrent systems. However, many real-world systems are inherently probabilistic as well as resource-bounded,
and there is no straightforward way of reasoning
about their unpredictable behaviours. In this paper,
we propose a logic for reasoning about coalitional
power under resource constraints in the probabilistic setting. We extend RB-ATL with probabilistic reasoning and provide a standard algorithm for
the model-checking problem of the resulting logic
Probabilistic Resource-Bounded ATL (pRB-ATL)